From a96346e308f93d2e6c385c3b0ce46fa6b27b0556 Mon Sep 17 00:00:00 2001 From: Thomas Sewell Date: Thu, 26 May 2016 17:51:53 +1000 Subject: [PATCH] SELFOUR-444: Finished InfoFlow and DRefine. --- lib/EquivValid.thy | 2 +- proof/access-control/Access.thy | 36 +- proof/drefine/Arch_DR.thy | 11 +- proof/drefine/Finalise_DR.thy | 8 +- proof/drefine/Syscall_DR.thy | 9 +- proof/drefine/Untyped_DR.thy | 928 +++++++++---------- proof/infoflow/ADT_IF.thy | 30 +- proof/infoflow/Arch_IF.thy | 26 +- proof/infoflow/Decode_IF.thy | 16 +- proof/infoflow/FinalCaps.thy | 176 ++-- proof/infoflow/IRQMasks_IF.thy | 7 +- proof/infoflow/PasUpdates.thy | 7 +- proof/infoflow/Retype_IF.thy | 870 ++++++++--------- proof/infoflow/Syscall_IF.thy | 28 +- proof/invariant-abstract/ARM/ArchArch_AI.thy | 5 +- proof/invariant-abstract/Retype_AI.thy | 36 + 16 files changed, 1009 insertions(+), 1186 deletions(-) diff --git a/lib/EquivValid.thy b/lib/EquivValid.thy index 9e6906e27..9a2cfce01 100644 --- a/lib/EquivValid.thy +++ b/lib/EquivValid.thy @@ -494,7 +494,7 @@ lemma liftME_ev: lemma whenE_ev: assumes a: "b \ equiv_valid_inv I A P m" - shows "equiv_valid_inv I A P (whenE b m)" + shows "equiv_valid_inv I A (\s. b \ P s) (whenE b m)" unfolding whenE_def by (auto intro: a returnOk_ev_pre) lemma whenE_throwError_bindE_ev: diff --git a/proof/access-control/Access.thy b/proof/access-control/Access.thy index e443930a9..30e6c1152 100644 --- a/proof/access-control/Access.thy +++ b/proof/access-control/Access.thy @@ -1596,41 +1596,7 @@ lemma cap_cur_auth_caps_of_state: \ pas_cap_cur_auth aag cap" by (metis cap_auth_caps_of_state) -lemma new_range_subset': - assumes al: "is_aligned (ptr :: 'a :: len word) sz" and al': "is_aligned x sz'" - and szv: "sz' \ sz" and xsz: "x < 2 ^ sz" - shows "{ptr + x .. (ptr + x) + 2 ^ sz' - 1} \ {ptr .. ptr + 2 ^ sz - 1}" - using al -proof (rule is_aligned_get_word_bits) - assume p0: "ptr = 0" and szv': "len_of TYPE ('a) \ sz" - hence "(2 :: 'a word) ^ sz = 0" by simp - - thus ?thesis using p0 - apply - - apply (erule ssubst) - apply simp - done -next - assume szv': "sz < len_of TYPE('a)" - - hence blah: "2 ^ (sz - sz') < (2 :: nat) ^ len_of TYPE('a)" - using szv - apply - - apply (rule power_strict_increasing, simp+) - done - show ?thesis using szv szv' - apply (intro range_subsetI) - apply (rule is_aligned_no_wrap' [OF al xsz]) - apply (simp only: add_diff_eq[symmetric]) - apply (subst add.assoc, rule word_plus_mono_right) - apply (subst iffD1 [OF le_m1_iff_lt]) - apply (simp add: p2_gt_0 word_bits_conv) - apply (rule is_aligned_add_less_t2n[OF al' _ szv xsz]) - apply simp - apply (simp add: field_simps szv al is_aligned_no_overflow) - done -qed - +lemmas new_range_subset' = aligned_range_offset_subset lemmas ptr_range_subset = new_range_subset' [folded ptr_range_def] lemma pbfs_less_wb: diff --git a/proof/drefine/Arch_DR.thy b/proof/drefine/Arch_DR.thy index 238fbb2d0..921d85c8e 100644 --- a/proof/drefine/Arch_DR.thy +++ b/proof/drefine/Arch_DR.thy @@ -1931,12 +1931,9 @@ proof - set_cap_caps_no_overlap set_cap_no_overlap set_cap_cte_wp_at set_cap_cte_cap_wp_to) apply (simp add:region_in_kernel_window_def obj_bits_api_def default_arch_object_def) - apply (wp set_untyped_cap_caps_overlap_reserved get_cap_wp) - apply (rule hoare_strengthen_post) - apply (rule set_cap_device_and_range_aligned[where dev = False,simp]) - apply simp - apply simp - apply (wp set_untyped_cap_caps_overlap_reserved get_cap_wp) + apply (wp set_untyped_cap_caps_overlap_reserved get_cap_wp + set_cap_no_overlap set_cap_cte_wp_at + | strengthen exI[where x=cref])+ apply clarsimp apply clarsimp apply (intro set_eqI) @@ -1948,7 +1945,7 @@ proof - 2 \ page_bits" in hoare_gen_asm) apply (simp add: delete_objects_rewrite is_aligned_neg_mask_eq) apply (rule_tac Q="\_ s. - invs s \ valid_etcbs s \ pspace_no_overlap frame pageBits s \ + invs s \ valid_etcbs s \ pspace_no_overlap_range_cover frame pageBits s \ descendants_range_in (untyped_range (cap.UntypedCap False frame pageBits idx)) cref s \ cte_wp_at (op = (cap.UntypedCap False frame pageBits idx)) cref s \ cte_wp_at (op = cap.NullCap) cnode_ref s \ diff --git a/proof/drefine/Finalise_DR.thy b/proof/drefine/Finalise_DR.thy index 59adefd35..bfe03e09b 100644 --- a/proof/drefine/Finalise_DR.thy +++ b/proof/drefine/Finalise_DR.thy @@ -1842,12 +1842,12 @@ lemma dcorres_unmap_large_section: apply (simp add:pd_bits_def pageBits_def) apply (simp add:shiftr_shiftl1) apply (subst (asm) is_aligned_neg_mask_eq[where n = 2]) - apply (erule aligned_after_mask[OF aligned_add_aligned]) + apply (erule is_aligned_andI1[OF aligned_add_aligned]) apply (simp add:shiftl_t2n[symmetric,where n =2, simplified field_simps,simplified] is_aligned_shiftl_self) apply simp apply (subst (asm) is_aligned_neg_mask_eq[where n = 2]) - apply (erule aligned_after_mask[OF is_aligned_weaken]) + apply (erule is_aligned_andI1[OF is_aligned_weaken]) apply simp apply (subst (asm) and_mask_plus) apply (erule(1) lookup_pd_slot_aligned_6) @@ -1954,12 +1954,12 @@ lemma dcorres_unmap_large_page: apply (simp add:pt_bits_def pageBits_def) apply (simp add:shiftr_shiftl1) apply (subst (asm) is_aligned_neg_mask_eq[where n = 2]) - apply (erule aligned_after_mask[OF aligned_add_aligned]) + apply (erule is_aligned_andI1[OF aligned_add_aligned]) apply (simp add:shiftl_t2n[symmetric,where n =2, simplified field_simps,simplified] is_aligned_shiftl_self) apply simp apply (subst (asm) is_aligned_neg_mask_eq[where n = 2]) - apply (erule aligned_after_mask[OF is_aligned_weaken]) + apply (erule is_aligned_andI1[OF is_aligned_weaken]) apply simp apply (subst (asm) and_mask_plus) apply simp diff --git a/proof/drefine/Syscall_DR.thy b/proof/drefine/Syscall_DR.thy index 19acf3b57..991031296 100644 --- a/proof/drefine/Syscall_DR.thy +++ b/proof/drefine/Syscall_DR.thy @@ -689,12 +689,9 @@ lemma perform_invocation_corres: apply (case_tac i') apply (simp_all add: translate_invocation_def split: Invocations_A.invocation.splits) (* untyped *) - apply (simp add:liftE_bindE) - apply (simp add:liftE_def returnOk_def) - apply (rule corres_guard_imp[OF corres_split']) - apply (rule invoke_untyped_corres) - apply (rule corres_trivial,simp) - apply wp + apply (simp add: liftME_def[symmetric]) + apply (rule corres_guard_imp, rule invoke_untyped_corres) + apply clarsimp apply clarsimp (* send_ipc *) diff --git a/proof/drefine/Untyped_DR.thy b/proof/drefine/Untyped_DR.thy index 14fac5ead..417d2228c 100644 --- a/proof/drefine/Untyped_DR.thy +++ b/proof/drefine/Untyped_DR.thy @@ -245,7 +245,7 @@ lemma valid_page_cap_imp_valid_buf: lemma freeMemory_dcorres: "is_aligned ptr bits \ 2 \ bits \ bits < word_bits \ dcorres dc (\_. True) - (pspace_no_overlap ptr bits and valid_objs and valid_etcbs) + (pspace_no_overlap_range_cover ptr bits and valid_objs and valid_etcbs) (return rv) (do_machine_op (freeMemory ptr bits))" apply (clarsimp simp add: corres_underlying_def split_def return_def) apply (rename_tac s t) @@ -387,13 +387,13 @@ definition translate_untyped_invocation :: "Invocations_A.untyped_invocation \ cdl_untyped_invocation" where "translate_untyped_invocation x \ - case x of Invocations_A.Retype cref ptr_base ptr tp us slots dev + case x of Invocations_A.Retype cref reset ptr_base ptr tp us slots dev \ cdl_untyped_invocation.Retype (transform_cslot_ptr cref ) (translate_object_type tp) us (map transform_cslot_ptr slots) - (ptr_base \ ptr) (length slots) " + (\ reset) (length slots)" definition "retype_transform_obj_ref type sz ptr @@ -510,7 +510,7 @@ lemma transform_none_to_untyped: done lemma retype_transform_obj_ref_available: - "\pspace_no_overlap ptr sz s'; s = transform s'; valid_pspace s'; valid_idle s'; + "\pspace_no_overlap_range_cover ptr sz s'; s = transform s'; valid_pspace s'; valid_idle s'; range_cover ptr sz (obj_bits_api ty us) n; y \ set (retype_addrs ptr ty n us)\ \ retype_transform_obj_ref ty us y \ @@ -519,12 +519,13 @@ lemma retype_transform_obj_ref_available: apply (rule transform_none_to_untyped, simp) apply (rule ccontr, clarsimp) apply (drule(1) retype_addrs_range_subset[where p = y]) - apply (drule_tac S = "{x}" in pspace_no_overlap_obj_range) - apply assumption - apply (erule subset_trans[rotated]) - apply (clarsimp simp:obj_bits_api_def) + apply (drule(1) pspace_no_overlap_obj_range) + apply (simp only: field_simps) + apply (drule(1) disjoint_subset2) + apply (clarsimp simp:obj_bits_api_def) apply (drule p_in_obj_range) apply clarsimp+ + apply auto[1] apply (drule(2) pspace_no_overlap_into_Int_none) apply (clarsimp simp: transform_def restrict_map_def map_add_def transform_objects_def split: if_splits option.splits) @@ -580,7 +581,7 @@ lemma retype_region_dcorres: "dcorres (\rv rv'. rv = map (retype_transform_obj_ref type us) rv' \ rv' = retype_addrs ptr type n us) \ - (\s. pspace_no_overlap ptr sz s \ invs s + (\s. pspace_no_overlap_range_cover ptr sz s \ invs s \ range_cover ptr sz (obj_bits_api type us) n \ (type = Structures_A.Untyped \ 4 \ us) \ (type = Structures_A.CapTableObject \ us \ 0)) @@ -691,56 +692,6 @@ lemma clearMemory_unused_corres_noop: apply (wp | simp)+ done -lemma dcorres_create_word_objects: - "\ 0 < n; ty \ ArchObject ` {SmallPageObj, LargePageObj, SectionObj, SuperSectionObj}; - xsz = obj_bits_api ty us \ - \ dcorres dc (\_. True) - (\s. (\x\set (retype_addrs ptr ty n us). - obj_at (\ko. ko = Retype_A.default_object ty dev us) x s \ - (\cap\ ran (caps_of_state s). x\ (obj_refs cap))) \ - range_cover ptr sz (obj_bits_api ty us) n \ - valid_objs s \ pspace_aligned s \ pspace_distinct s \ valid_idle s \ valid_etcbs s) - (return ()) (create_word_objects ptr n xsz dev)" - apply (clarsimp simp:create_word_objects_def reserve_region_def mapM_x_mapM) - apply (subst do_machine_op_bind) - apply ((wp empty_fail_mapM empty_fail_bind - | simp add:clearMemory_def mapM_x_mapM ef_storeWord)+)[2] - apply (subst dom_mapM) - apply ((wp empty_fail_mapM empty_fail_bind - | simp add:clearMemory_def mapM_x_mapM ef_storeWord)+)[1] - apply (rule corres_dummy_return_pl) - apply (rule dcorres_expand_pfx) - apply (rule corres_guard_imp) - apply (rule dcorres_unless_r) - apply (rule corres_split[OF corres_trivial]) - apply simp - apply (rule corres_mapM_to_mapM_x) - apply (rule_tac P=\ and P'="P" and S = "{(x,y). y \ set M}" for P M - in corres_mapM_x[where f="\_. return ()", OF _ _ _ refl, - simplified mapM_x_return]) - apply clarsimp - apply (rule clearMemory_unused_corres_noop) - apply simp - apply simp - apply simp - apply wp - apply (wp hoare_vcg_ball_lift | simp)+ - apply (clarsimp simp:zip_same_conv_map retype_addrs_def ptr_add_def image_def shiftl_t2n) - apply (rule_tac x = "unat x" in bexI) - apply simp - apply clarsimp - apply (rule unat_less_helper) - apply (subst le_m1_iff_lt[THEN iffD1,symmetric]) - apply (drule range_cover_not_zero[rotated]) - apply simp - apply (simp add:word_neq_0_conv) - apply simp - apply wp - apply simp - apply simp - apply fastforce - done - lemma init_arch_objects_corres_noop: notes [simp del] = atLeastAtMost_iff atLeastatMost_subset_iff shows @@ -754,63 +705,12 @@ lemma init_arch_objects_corres_noop: obj_refs cap \ {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) \ valid_objs s \ pspace_aligned s \ pspace_distinct s \ valid_idle s \ valid_etcbs s) (return ()) - (init_arch_objects ty ptr n obj_sz refs dev)" + (init_arch_objects ty ptr n obj_sz refs)" apply (simp add: init_arch_objects_def split: Structures_A.apiobject_type.split aobject_type.split) apply (simp add: dcorres_machine_op_noop[THEN corres_guard_imp] cleanCacheRange_PoU_def machine_op_lift) apply safe - apply (rule corres_guard_imp) - apply (erule corres_guard_imp[OF dcorres_create_word_objects - [where sz = sz and us = obj_sz and ty = "ArchObject SmallPageObj"]]) - apply simp - apply (clarsimp simp:obj_bits_api_def arch_kobj_size_def default_arch_object_def) - apply simp - apply assumption - apply simp - apply (clarsimp simp:null_filter_def) - apply (drule(1) bspec) - apply (drule_tac x = cap in bspec) - apply (erule ranE) - apply (rule_tac a = xa in ranI) - apply clarsimp - apply (erule(1) in_empty_interE) - apply (clarsimp dest!:retype_addrs_subset_ptr_bits simp:field_simps,blast) - apply (rule corres_guard_imp) - apply (erule corres_guard_imp[OF dcorres_create_word_objects - [where sz = sz and us = obj_sz and ty = "ArchObject LargePageObj"]]) - apply (clarsimp simp:obj_bits_api_def arch_kobj_size_def default_arch_object_def)+ - apply assumption+ - apply (clarsimp simp:null_filter_def) - apply (drule(1) bspec,drule_tac x = cap in bspec) - apply (erule ranE,rule_tac a = xa in ranI) - apply clarsimp - apply (erule(1) in_empty_interE) - apply (clarsimp dest!:retype_addrs_subset_ptr_bits simp:field_simps,blast) - apply (rule corres_guard_imp) - apply (erule corres_guard_imp[OF dcorres_create_word_objects - [where sz = sz and us = obj_sz and ty = "ArchObject SectionObj"]]) - apply (clarsimp simp:obj_bits_api_def arch_kobj_size_def default_arch_object_def)+ - apply assumption+ - apply (clarsimp simp:null_filter_def) - apply (drule(1) bspec,drule_tac x = cap in bspec) - apply (erule ranE,rule_tac a = xa in ranI) - apply clarsimp - apply (erule(1) in_empty_interE) - apply (clarsimp dest!:retype_addrs_subset_ptr_bits simp:field_simps,blast) - apply (rule corres_guard_imp) - apply (erule corres_guard_imp[OF dcorres_create_word_objects - [where sz = sz and us = obj_sz and ty = "ArchObject SuperSectionObj"]]) - apply (clarsimp simp:obj_bits_api_def arch_kobj_size_def default_arch_object_def)+ - apply assumption+ - apply (clarsimp simp:null_filter_def) - apply (drule(1) bspec,drule_tac x = cap in bspec) - apply (erule ranE,rule_tac a = xa in ranI) - apply clarsimp - apply (erule(1) in_empty_interE) - apply (clarsimp dest!:retype_addrs_subset_ptr_bits simp:field_simps,blast) - apply (rule corres_guard_imp[OF dcorres_machine_op_noop]) - apply (wp mapM_x_wp' | simp)+ apply (simp add:mapM_x_mapM) apply (rule corres_guard_imp) apply (rule corres_split_noop_rhs) @@ -1071,7 +971,7 @@ lemma generate_object_ids_exec: \ range_cover ptr sz (obj_bits_api ty us) n \ is_aligned ptr (obj_bits_api ty us) \ {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1} \ free_range ) - and (pspace_no_overlap ptr sz) and valid_pspace and valid_idle and P') + and (pspace_no_overlap_range_cover ptr sz) and valid_pspace and valid_idle and P') (do t \ generate_object_ids n (translate_object_type ty) free_range; f t @@ -1170,12 +1070,12 @@ lemma delete_objects_idle_thread[wp]: lemma update_available_range_dcorres: "dcorres dc \ ( K(\idx. untyped_cap = transform_cap (cap.UntypedCap dev ptr sz idx) \ free_range_of_untyped idx' sz ptr \ new_range - set oids) - and valid_idle and (\s. cref \ idle_thread s) and valid_etcbs) + and valid_idle and (\s. fst cref \ idle_thread s) and valid_etcbs) (update_available_range new_range oids - (transform_cslot_ptr (cref, oref)) untyped_cap) + (transform_cslot_ptr cref) untyped_cap) (CSpaceAcc_A.set_cap (cap.UntypedCap dev ptr sz idx') - (cref, oref))" + cref)" apply (rule dcorres_expand_pfx) apply (clarsimp simp:update_available_range_def) apply (rule corres_guard_imp) @@ -1225,22 +1125,22 @@ lemma le_p2_minus_1: done lemma free_range_of_untyped_subseteq': - "\a \ a';is_aligned ptr sz; sz < 32\ \ free_range_of_untyped a' sz (ptr::word32) \free_range_of_untyped a sz (ptr::word32)" + "\a \ a'; is_aligned ptr sz; sz < size (ptr)\ + \ free_range_of_untyped a' sz ptr \free_range_of_untyped a sz ptr" apply (clarsimp simp:free_range_of_untyped_def) apply (rule word_plus_mono_right) apply (drule le_p2_minus_1) apply (rule of_nat_mono_maybe_le[THEN iffD1,rotated -1]) apply simp apply (erule less_le_trans) - apply (rule power_increasing,simp+)[1] + apply (simp add: word_size) apply (drule(1) le_less_trans) apply (erule less_le_trans) - apply (rule power_increasing,simp+) + apply (simp add: word_size) apply (erule is_aligned_no_wrap') apply (rule word_of_nat_less) apply (drule le_p2_minus_1) - apply (simp add:unat_power_lower32[unfolded word_bits_def] - word_bits_def) + apply (simp add: word_size) done lemma retype_transform_obj_ref_not_empty: @@ -1308,374 +1208,417 @@ lemma free_range_of_untyped_pick_retype_addrs: apply simp done +lemma clearMemory_corres_noop: + "full_sz = 2 ^ sz \ is_aligned p sz \ 2 \ sz + \ sz < word_bits + \ dcorres dc \ + (pspace_no_overlap {p .. p + 2 ^ sz - 1} and valid_objs and valid_etcbs) + (return ()) + (do_machine_op (clearMemory p full_sz))" + apply (simp add: clearMemory_def freeMemory_def[symmetric] + do_machine_op_bind empty_fail_freeMemory) + apply (rule corres_guard_imp) + apply (rule corres_add_noop_lhs) + apply (rule corres_split_nor[OF _ freeMemory_dcorres]) + apply (rule dcorres_machine_op_noop) + apply (wp | simp)+ + apply (clarsimp simp: is_aligned_neg_mask_eq field_simps) + done + +lemma mapME_x_upt_length_ys: + "mapME_x (\_. f) [0 ..< length ys] + = mapME_x (\_. f) ys" + by (metis mapME_x_map_simp[where f="\_. ()" and m="\_. m" for m, + unfolded o_def] map_replicate_const length_upt minus_nat.diff_0) + +lemma monadic_set_cap_id: + "monadic_rewrite False True + (cte_wp_at (op = cap) p) + (set_cap cap p) (return ())" + by (clarsimp simp: monadic_rewrite_def set_cap_id return_def) + +lemmas monadic_set_cap_id2 + = monadic_rewrite_transverse[OF monadic_set_cap_id monadic_rewrite_refl] + +lemma monadic_rewrite_corres_rhs: + "\ monadic_rewrite False True Q c c'; + corres_underlying R F F' r P P' a c' \ + \ corres_underlying R F F' r P (P' and Q) a c" + apply (clarsimp simp: corres_underlying_def monadic_rewrite_def) + apply fastforce + done + +(* FIXME: move *) +lemma mapME_x_append: + "mapME_x f (xs @ ys) = (doE mapME_x f xs; mapME_x f ys odE)" + apply (induct xs) + apply (simp add: mapME_x_Nil) + apply (simp add: mapME_x_Cons bindE_assoc) + done + +lemma reset_untyped_cap_corres: + "dcorres (dc \ dc) \ (invs and valid_etcbs and ct_active + and cte_wp_at (\cap. is_untyped_cap cap \ free_index_of cap = idx) cref + and (\s. descendants_of cref (cdt s) = {})) + (Untyped_D.reset_untyped_cap (transform_cslot_ptr cref)) + (Retype_A.reset_untyped_cap cref)" + apply (rule dcorres_expand_pfx) + apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps) + apply (simp add: Untyped_D.reset_untyped_cap_def reset_untyped_cap_def + liftE_bindE) + apply (rule corres_guard_imp) + apply (rule corres_split[OF _ get_cap_corres]) + apply (rule_tac F="is_untyped_cap capa \ cap_aligned capa + \ bits_of capa > 2 \ free_index_of capa \ 2 ^ bits_of capa" + in corres_gen_asm2) + apply (rule corres_split_nor) + prefer 2 + apply (rule delete_objects_dcorres) + apply (clarsimp simp: is_cap_simps bits_of_def) + apply (rule corres_if_rhs) + apply (rule_tac x=0 in select_pick_corres_asm) + apply simp + apply (simp add: mapME_x_Nil) + apply (rule corres_add_noop_lhs) + apply (rule corres_split_nor) + prefer 2 + apply (rule dcorres_unless_r) + apply (rule clearMemory_corres_noop[OF refl]) + apply (clarsimp simp: is_cap_simps cap_aligned_def bits_of_def) + apply (clarsimp simp: is_cap_simps bits_of_def free_range_of_untyped_def) + apply (clarsimp simp: is_cap_simps cap_aligned_def bits_of_def) + apply (rule corres_trivial, simp) + apply (rule set_cap_corres) + apply (clarsimp simp: is_cap_simps bits_of_def free_range_of_untyped_def) + apply simp + apply (wp | simp add: unless_def)+ + apply (rule_tac x="length xs" for xs in select_pick_corres_asm) + apply simp + apply (simp add: mapME_x_upt_length_ys) + apply (rule corres_dummy_returnOk_r) + apply (rule corres_splitEE) + prefer 2 + apply (rule_tac P="\\" and P'="\_. valid_objs + and valid_etcbs and pspace_no_overlap (untyped_range capa) + and valid_idle and (\s. idle_thread s \ fst cref) + and cte_wp_at (\cp. \idx. cp = free_index_update (\_. idx) capa) cref" + in mapME_x_corres_same_xs[OF _ _ _ refl]) + apply (rule corres_guard_imp) + apply (rule corres_add_noop_lhs) + apply (rule corres_split_nor[OF _ clearMemory_corres_noop[OF refl]]) + apply (rule_tac x="available_range (transform_cap + (free_index_update (\_. x * 2 ^ reset_chunk_bits) capa))" + in select_pick_corres_asm) + apply (clarsimp simp: is_cap_simps bits_of_def free_index_of_def) + apply (strengthen free_range_of_untyped_subseteq') + apply (strengthen order_trans[OF free_range_of_untyped_subseteq'[where a=0]]) + apply (simp add: cap_aligned_def free_range_of_untyped_def + word_bits_def word_size) + apply (rule corres_split[OF _ set_cap_corres]) + apply (subst alternative_com) + apply (rule throw_or_return_preemption_corres[where P=\ and P'=\]) + apply (clarsimp simp: is_cap_simps bits_of_def) + apply simp + apply wp + apply (clarsimp simp add: is_cap_simps cap_aligned_def bits_of_def + aligned_add_aligned is_aligned_shiftl) + apply (simp add: reset_chunk_bits_def) + apply (simp add: reset_chunk_bits_def word_bits_def) + apply (wp hoare_vcg_all_lift hoare_vcg_const_imp_lift + preemption_point_inv' set_cap_no_overlap + update_untyped_cap_valid_objs set_cap_idle + | simp)+ + apply (clarsimp simp: is_cap_simps bits_of_def cap_aligned_def) + apply (erule pspace_no_overlap_subset) + apply (rule aligned_range_offset_subset, simp_all add: is_aligned_shiftl)[1] + apply (rule shiftl_less_t2n[OF word_of_nat_less]) + apply simp + apply (simp add: word_bits_def) + apply (rule hoare_pre, wp) + apply simp + apply (rule hoare_pre) + apply (wp hoare_vcg_all_lift hoare_vcg_const_imp_lift + update_untyped_cap_valid_objs set_cap_no_overlap + set_cap_idle preemption_point_inv' + set_cap_cte_wp_at + | simp)+ + apply (clarsimp simp: cte_wp_at_caps_of_state exI + is_cap_simps bits_of_def) + apply (frule(1) cte_wp_at_valid_objs_valid_cap[OF caps_of_state_cteD]) + apply (clarsimp simp: valid_cap_simps cap_aligned_def + valid_untyped_pspace_no_overlap + free_index_of_def) + apply (simp add: returnOk_liftE) + apply (rule monadic_rewrite_corres_rhs, + rule_tac cap="free_index_update (\_. 0) capa" + and p=cref in monadic_set_cap_id2) + apply (rule set_cap_corres[unfolded dc_def]) + apply (clarsimp simp: is_cap_simps free_range_of_untyped_def) + apply simp + apply wp + apply (rule_tac P="valid_etcbs + and valid_idle and (\s. idle_thread s \ fst cref) + and cte_wp_at (op = capa) cref" + in hoare_trivE_R) + apply (case_tac "free_index_of capa = 0") + apply (simp add: mapME_x_Nil) + apply wp + apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps + free_index_of_def) + apply (subst upt_conv_Cons) + apply simp + apply (simp add: mapME_x_append mapME_x_Cons mapME_x_Nil bindE_assoc) + apply (rule hoare_pre) + apply (wp preemption_point_inv' set_cap_idle + set_cap_cte_wp_at | simp + | (wp_once mapME_x_inv_wp, rule hoare_pre))+ + apply (clarsimp simp: is_cap_simps bits_of_def cte_wp_at_caps_of_state) + apply (simp del: hoare_TrueI) + apply wp + apply (wp add: hoare_vcg_const_imp_lift get_cap_wp + | simp + | strengthen invs_valid_objs invs_valid_idle)+ + apply (clarsimp simp: cte_wp_at_caps_of_state + descendants_range_def2) + apply (cases cref, simp) + apply (strengthen exI[mk_strg I] empty_descendants_range_in[mk_strg I E] + refl)+ + apply (clarsimp simp: is_cap_simps bits_of_def free_index_of_def + ) + apply ((strengthen refl)+)? + apply (frule cte_wp_at_valid_objs_valid_cap[OF caps_of_state_cteD], + clarsimp+) + apply (clarsimp simp: valid_cap_simps) + apply (frule if_unsafe_then_capD[OF caps_of_state_cteD], clarsimp+) + apply (frule(1) ex_cte_cap_protects[OF _ caps_of_state_cteD _ _ order_refl], + simp add: empty_descendants_range_in, clarsimp+) + apply (auto simp: not_idle_thread_def + dest!: valid_idle_has_null_cap[rotated -1]) + done + +lemma range_le_free_range_of_untyped: + "range_cover (ptr::word32) sz sbit n + \ n \ 0 + \ idx \ unat (ptr && mask sz) + \ {ptr..ptr + of_nat n * 2 ^ sbit - 1} + \ free_range_of_untyped idx sz (ptr && ~~ mask sz)" + apply (rule order_trans, erule(1) range_cover_subset') + apply (clarsimp simp: free_range_of_untyped_def + split del: split_if del: subsetI) + apply (subst if_P) + prefer 2 + apply (rule range_subsetI, simp_all) + apply (subst word_plus_and_or_coroll2[symmetric,where w = "mask sz" and t = ptr], + subst add.commute, + rule word_add_le_mono2) + apply (simp add: word_of_nat_le) + apply (simp only: no_olen_add_nat[symmetric] word_plus_and_or_coroll2 word_and_le2) + apply (erule order_trans) + apply (rule nat_le_Suc_less_imp) + apply (rule word_unat_mask_lt) + apply (simp add: range_cover_def word_size) + done + lemma invoke_untyped_corres: - "dcorres dc (\_. True) + "dcorres (dc \ dc) (\_. True) (invs and ct_active and valid_untyped_inv untyped_invocation and valid_etcbs) (Untyped_D.invoke_untyped (translate_untyped_invocation untyped_invocation)) (Retype_A.invoke_untyped untyped_invocation)" apply (rule dcorres_expand_pfx) + apply (clarsimp simp only: valid_untyped_inv_wcap) apply (cases untyped_invocation) - apply (clarsimp simp del:invoke_untyped.simps) - apply (rename_tac s cref oref ptr tp us slots dev sz idx) + apply (rename_tac s s' sz idx creforef reset ptr ptr' tp us slots dev) proof - - fix cref oref ptr tp us slots s dev sz idx - assume cte_wp_at : "cte_wp_at (\c. c = cap.UntypedCap dev (ptr && ~~ mask sz) sz idx) (cref,oref) (s :: det_ext state)" - have cte_at: "cte_wp_at (op = (cap.UntypedCap dev (ptr && ~~ mask sz) sz idx)) (cref,oref) s" (is "?cte_cond s") - using cte_wp_at by (simp add:cte_wp_at_caps_of_state) - assume desc_range: "ptr = ptr && ~~ mask sz \ descendants_range_in {ptr..ptr + 2 ^ sz - 1} (cref,oref) s" - assume misc : "distinct slots" "tp = Structures_A.CapTableObject \ 0 < (us::nat)" - " tp = Structures_A.Untyped \ 4 \ (us::nat)" - " idx \ unat (ptr && mask sz) \ ptr = ptr && ~~ mask sz" - " invs s" "valid_etcbs s" "tp \ ArchObject ASIDPoolObj" - " \slot\set slots. cte_wp_at (op = cap.NullCap) slot s \ ex_cte_cap_wp_to is_cnode_cap slot s \ real_cte_at slot s" - " ct_active s" - assume cover : "range_cover ptr sz (obj_bits_api tp us) (length slots)" - assume vslot : "slots\ []" + fix s cref reset ptr ptr' tp us slots sz idx dev + assume vui1: "valid_untyped_inv_wcap untyped_invocation + (Some (case untyped_invocation of + Invocations_A.untyped_invocation.Retype slot reset ptr_base ptr ty us slots dev \ + cap.UntypedCap dev (ptr && ~~ mask sz) sz idx)) s" + and ui: "untyped_invocation = + Invocations_A.Retype cref reset ptr' ptr tp us slots dev" + and etc: "valid_etcbs s" "invs s" "ct_active s" - note blah[simp del] = usable_untyped_range.simps atLeastAtMost_iff + note vui = vui1[simplified ui Invocations_A.untyped_invocation.simps] + + have ptrs: "ptr' = ptr && ~~ mask sz" + using vui + by (auto simp: ui cte_wp_at_caps_of_state word_bw_assocs) + + have cover: "range_cover ptr sz (obj_bits_api tp us) (length slots)" + and vslot: "slots \ []" "distinct slots" + and misc: "tp = Structures_A.apiobject_type.CapTableObject \ 0 < us" + "tp = Structures_A.apiobject_type.Untyped \ 4 \ us" + using vui + by (auto simp: ui cte_wp_at_caps_of_state) + + have vcap: "s \ cap.UntypedCap dev (ptr && ~~ mask sz) sz idx" + using vui etc + by (auto simp: ui cte_wp_at_caps_of_state + dest!: caps_of_state_valid[rotated]) + + note [simp del] = usable_untyped_range.simps atLeastAtMost_iff atLeastatMost_subset_iff split_paired_Ex - have [simp]:"(cref, oref) \ set slots" - using cte_wp_at misc by(clarsimp simp:cte_wp_at_caps_of_state) - - have not_idle:"not_idle_thread cref s" - using cte_wp_at misc - apply - - apply (rule ccontr) - apply (clarsimp simp:not_idle_thread_def cte_wp_at_caps_of_state) - apply (drule valid_idle_has_null_cap[rotated -1]) - apply clarsimp+ - done - have pf: "invoke_untyped_proofs s (cref,oref) ptr tp us slots sz idx dev" - using cte_wp_at desc_range misc cover vslot - apply (clarsimp simp:invoke_untyped_proofs_def cte_wp_at_caps_of_state) - apply (drule(1) bspec) - apply (clarsimp elim!:ex_cte_cap_wp_to_weakenE) - done - - have pf_arch: "invoke_untyped_proofs_arch s (cref,oref) ptr tp us slots sz idx dev" - using cte_wp_at desc_range misc cover vslot - apply (clarsimp simp:invoke_untyped_proofs_arch_def invoke_untyped_proofs_def cte_wp_at_caps_of_state) - apply (drule(1) bspec) - apply (clarsimp elim!:ex_cte_cap_wp_to_weakenE) - done - - note cte_wp_at_machine_state[simp del] - note set_cap_free_index_invs_spec = set_free_index_invs[where cap = "cap.UntypedCap dev (ptr && ~~ mask sz) sz idx" - ,unfolded free_index_update_def free_index_of_def,simplified] - - note subset_stuff[simp] = invoke_untyped_proofs.subset_stuff[OF pf] - note descendants_range[simp] = invoke_untyped_proofs.descendants_range[OF pf] - note ps_no_overlap[simp] = invoke_untyped_proofs.ps_no_overlap[OF pf] - note caps_no_overlap[simp] = invoke_untyped_proofs.caps_no_overlap[OF pf] - note slots_invD = invoke_untyped_proofs.slots_invD[OF pf] - note kernel_window_inv = invoke_untyped_proofs_arch.kernel_window_inv[OF pf_arch] - note ptr_0[simp] = invoke_untyped_proofs.not_0_ptr - - have nidx[simp]: "\m. ptr + m - (ptr && ~~ mask sz) - = (ptr && mask sz) + m" - apply (subst word_plus_and_or_coroll2[symmetric,where w = "mask sz" and t = ptr]) - apply simp - done - - have non_detype_idx_le[simp]: "ptr \ ptr && ~~ mask sz \ idx < 2^sz" - using misc cover - apply clarsimp - apply (frule le_mask_le_2p) - apply (simp add:range_cover_def[where 'a=32, folded word_bits_def])+ - done - - have in_free_range: - "ptr \ ptr && ~~ mask sz \ {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} - \ free_range_of_untyped idx sz (ptr && ~~ mask sz)" - using misc - apply (clarsimp simp:free_range_of_untyped_def nat_le_Suc_less_imp atLeastatMost_subset_iff) - apply (subgoal_tac "(ptr && ~~ mask sz) + of_nat idx \ (ptr && ~~ mask sz) + (ptr && mask sz)") - apply (simp add:mask_out_sub_mask) - apply (rule word_plus_mono_right) - apply (simp add:word_of_nat_le) - apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask]) - apply (rule le_refl) - apply (rule and_mask_less') - apply (rule range_cover.sz[OF cover]) - done - - have idx_compare: - "ptr \ ptr && ~~ mask sz \ - idx \ unat ((ptr && mask sz) + of_nat (length slots) * 2 ^ obj_bits_api tp us)" - using misc - apply (cut_tac range_cover_unat[OF cover]) - apply simp - done - - note neg_mask_add_mask = word_plus_and_or_coroll2[symmetric,where w = "mask sz" and t = ptr,symmetric] - - have [simp]: "ptr &&~~ mask sz = ptr \ {ptr + of_nat k |k. k < 2 ^ sz} = {ptr .. ptr + 2 ^ sz - 1}" - using cover - apply - - apply (rule intvl_range_conv) - apply (simp add:is_aligned_neg_mask_eq') - apply (simp add:range_cover_def) - done - - have detype_valid_etcbs: "\ valid_etcbs s; ptr && ~~ mask sz = ptr \ \ valid_etcbs (detype {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} (clear_um {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s))" - apply (clarsimp simp: valid_etcbs_def st_tcb_at_def is_etcb_at_def detype_def detype_ext_def - st_tcb_at_kh_def obj_at_kh_def obj_at_def clear_um_def) - done - - note msimp[simp add] = misc getObjectSize_def_eq neg_mask_add_mask - - show "dcorres dc (op = (transform s)) (op = s) + show "dcorres (dc \ dc) (op = (transform s)) (op = s) (Untyped_D.invoke_untyped - (translate_untyped_invocation - (Invocations_A.untyped_invocation.Retype (cref, oref) (ptr && ~~ mask sz) ptr tp us slots dev))) - (Retype_A.invoke_untyped - (Invocations_A.untyped_invocation.Retype (cref, oref) (ptr && ~~ mask sz) ptr tp us slots dev))" - using not_idle + (translate_untyped_invocation untyped_invocation)) + (Retype_A.invoke_untyped untyped_invocation)" apply (clarsimp simp: Untyped_D.invoke_untyped_def mapM_x_def - translate_untyped_invocation_def) - apply (clarsimp simp:unless_def) - apply (case_tac "ptr && ~~ mask sz = ptr") - apply (rule corres_guard_imp) - apply (rule corres_split[OF _ get_cap_corres] ) - apply (rule corres_split[OF _ corres_when]) - apply (rule generate_object_ids_exec[where ptr = ptr and us = us and sz = sz]) - apply (simp add:generate_object_ids_def) - apply (rule corres_split[OF _ update_available_range_dcorres]) - apply simp - apply (rule corres_split[OF _ retype_region_dcorres[where sz = sz]]) - apply (rule corres_split_noop_rhs[OF _ init_arch_objects_corres_noop[where sz =sz]]) - apply (simp add: liftM_def[symmetric] mapM_x_def[symmetric] - zip_map1 zip_map2 o_def split_beta dc_def[symmetric]) - apply (rule_tac F = " (untyped_is_device (transform_cap cap)) = dev" in corres_gen_asm2) - apply clarify - apply (rule create_caps_loop_dcorres) - apply clarsimp - apply (erule retype_addrs_aligned[OF _ range_cover.aligned _ le_refl]) - apply (rule cover) - apply (rule range_cover_sz'[where 'a=32, folded word_bits_def, OF cover]) - apply (rule cover) - apply (simp add:misc vslot) - apply ((wp | simp add: mdb_cte_at_def | rule hoare_vcg_conj_lift, wps)+)[2] - apply (wp retype_region_aligned_for_init[where sz = sz] - retype_region_obj_at[THEN hoare_vcg_const_imp_lift] - retype_region_caps_of[where sza = "\_. sz"] - | simp add:misc)+ - apply (rule_tac Q="\rv s. cte_wp_at (op \ cap.NullCap) (cref, oref) s \ post_retype_invs tp rv s - \ idle_thread s \ fst ` set slots - \ (\slot\set slots. - cte_wp_at (op = cap.NullCap) slot s) \ valid_etcbs s - \ untyped_is_device (transform_cap cap) = dev" - in hoare_post_imp) - apply (simp add:post_retype_invs_def split:split_if_asm) - apply ((clarsimp dest!:set_zip_leftD - simp:image_def invs_def valid_state_def valid_mdb_def - elim!:cte_wp_at_weakenE | intro conjI | drule (1) bspec | drule(1) mdb_cte_atD[rotated])+)[2] - apply (wp retype_region_cte_at_other'[where sz= sz] retype_region_post_retype_invs[where sz = sz] - hoare_vcg_const_Ball_lift retype_region_aligned_for_init) - apply (clarsimp simp:conj_comms misc cover) - apply (rule_tac Q="\r s. - cte_wp_at (op = (cap.UntypedCap dev ptr sz (unat (of_nat (length slots) << obj_bits_api tp us)))) (cref, oref) s \ - invs s \ pspace_no_overlap ptr sz s \ caps_no_overlap ptr sz s \ - region_in_kernel_window {ptr..ptr + 2 ^ sz - 1} s \ - caps_overlap_reserved {ptr..ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} s \ - idle_thread s \ fst ` set slots \ cap_objects (transform_cap cap) = {ptr..ptr + (2 ^ sz - 1)} - \ untyped_is_device (transform_cap cap) = dev - \ (\x\set slots. cte_wp_at (op= cap.NullCap) x s) \ valid_etcbs s" - in hoare_strengthen_post[rotated]) - apply (clarsimp simp: invs_mdb invs_valid_pspace cte_wp_at_caps_of_state split_paired_Ex) - apply (rule conjI,fastforce) - apply (rule conjI,clarsimp) - apply (erule ranE) - apply (clarsimp simp:null_filter_def split:if_splits) - apply (frule_tac cap = capa in caps_of_state_ko[OF caps_of_state_valid]) - apply assumption - apply (elim disjE) - apply (clarsimp simp:cap_range_def is_cap_simps)+ - apply (rule disjointI) - apply clarsimp - apply (drule bspec,fastforce,clarsimp) - apply (drule_tac S = "{y}" in pspace_no_overlap_obj_range) - apply assumption - apply simp - apply (drule p_in_obj_range) - apply clarsimp+ - apply (intro exI conjI) - apply simp - apply simp - apply (clarsimp simp:cap_range_def p_assoc_help) - apply (rule_tac P = "cap = cap.UntypedCap dev (ptr && ~~ mask sz) sz idx" in hoare_gen_asm) - apply (simp add:bits_of_def region_in_kernel_window_def) - apply (wp set_cap_no_overlap hoare_vcg_ball_lift set_untyped_cap_invs_simple - set_cap_cte_wp_at set_cap_descendants_range_in set_cap_caps_no_overlap - set_untyped_cap_caps_overlap_reserved set_cap_cte_cap_wp_to) - apply simp - apply simp - apply (rule_tac F = "cap = cap.UntypedCap dev (ptr && ~~ mask sz) sz idx" in corres_gen_asm2) - apply (rule delete_objects_dcorres) - apply (rule set_eqI) - apply (clarsimp simp: bits_of_def image_def) - apply wp - apply (clarsimp simp:conj_comms) - apply (rule_tac P = "cap = cap.UntypedCap dev ptr sz idx \ sz \ word_bits - \ 2 \ sz" in hoare_gen_asm) - apply (clarsimp simp:delete_objects_rewrite bits_of_def) - apply (wp get_cap_wp | clarsimp | simp)+ - using cte_at invoke_untyped_proofs.detype_descendants_range_in[OF pf] descendants_range - misc invoke_untyped_proofs.cref_inv[OF pf] invoke_untyped_proofs.detype_invs[OF pf] - cover invoke_untyped_proofs.vc[OF pf] subset_stuff invoke_untyped_proofs.usable_range_disjoint[OF pf] - range_cover.sz[OF cover] range_cover.aligned[OF cover] detype_valid_etcbs - apply (clarsimp simp: detype_clear_um_independent conj_comms not_idle_thread_def - misc invs_valid_idle invs_valid_objs word_bits_def) - apply (clarsimp simp: cte_wp_at_caps_of_state range_cover.aligned - bits_of_def field_simps) - apply (intro conjI) - apply (simp add: valid_cap_simps) - apply fastforce - apply (clarsimp dest!: invs_valid_idle) - apply (clarsimp dest!: invs_valid_pspace) - apply (erule pspace_no_overlap_detype) - apply (clarsimp simp: invs_psp_aligned) - apply (clarsimp simp: invs_valid_objs) - apply (rule caps_no_overlap_detype,simp) - apply (rule invoke_untyped_proofs.idx_compare'[OF pf]) - apply (simp add: is_aligned_neg_mask_eq'[symmetric] is_aligned_mask) - apply (simp add: descendants_range_def2 untyped_range.simps) - apply fastforce - apply (simp add: clear_um_def detype_def) - apply (simp add: clear_um_def detype_def) - apply (clarsimp simp: clear_um_def kernel_window_inv) - apply (clarsimp simp: clear_um_def detype_def dest!: slots_invD) - apply (drule ex_cte_cap_to_not_idle) - apply (clarsimp simp: invs_valid_global_refs) - apply (simp add: invs_valid_idle) - apply (clarsimp simp:invs_irq_node) - apply simp - apply (drule(1) descendants_range_in_subseteq) - apply simp - apply (simp add: shiftl_t2n field_simps) - apply (clarsimp dest!:slots_invD) - apply (rule subseteq_set_minus) - apply (drule free_range_of_untyped_subseteq) - apply (simp add: shiftl_t2n field_simps - mask_out_sub_mask) - apply (drule free_range_of_untyped_pick_retype_addrs) - apply (simp add: vslot) - apply simp - apply (simp add: valid_etcbs_def is_etcb_at_def st_tcb_at_def detype_def detype_ext_def clear_um_def st_tcb_at_kh_def obj_at_kh_def obj_at_def) + translate_untyped_invocation_def + ui ptrs invoke_untyped_def unlessE_whenE) apply (rule corres_guard_imp) - apply (rule corres_split[OF _ get_cap_corres] ) + apply (rule corres_split_norE) + prefer 2 + apply (rule corres_whenE, simp) + apply (rule reset_untyped_cap_corres[where idx=idx]) apply simp - apply (rule generate_object_ids_exec[where ptr = ptr and us = us and sz = sz and ty = tp]) - apply (rule corres_split[OF _ update_available_range_dcorres]) + apply simp + apply (rule corres_split[OF _ get_cap_corres]) apply simp - apply (rule corres_split[OF _ retype_region_dcorres[where sz = sz]]) - apply (rule corres_split_noop_rhs[OF _ init_arch_objects_corres_noop[where sz =sz]]) - apply (simp add: liftM_def[symmetric] mapM_x_def[symmetric] - zip_map1 zip_map2 o_def split_beta dc_def[symmetric]) + apply (rule generate_object_ids_exec[where ptr = ptr and us = us and sz = sz]) + apply simp + apply (rule corres_split[OF _ update_available_range_dcorres]) + apply simp + apply (rule corres_split[OF _ retype_region_dcorres[where sz = sz]]) + apply (rule corres_split_noop_rhs[OF _ init_arch_objects_corres_noop[where sz =sz]]) + apply (simp add: liftM_def[symmetric] mapM_x_def[symmetric] + zip_map1 zip_map2 o_def split_beta dc_def[symmetric]) apply (rule_tac F = " (untyped_is_device (transform_cap cap)) = dev" in corres_gen_asm2) apply clarify - apply (rule create_caps_loop_dcorres) - apply clarsimp - apply (erule retype_addrs_aligned[OF _ range_cover.aligned _ le_refl]) + apply (rule create_caps_loop_dcorres) + apply clarsimp + apply (erule retype_addrs_aligned[OF _ range_cover.aligned _ le_refl]) + apply (rule cover) + apply (rule range_cover_sz'[where 'a=32, folded word_bits_def, OF cover]) apply (rule cover) - apply (rule range_cover_sz'[where 'a=32, folded word_bits_def, OF cover]) - apply (rule cover) - apply (simp add:misc vslot) - apply ((wp | simp add: mdb_cte_at_def | rule hoare_vcg_conj_lift, wps)+)[2] - apply (wp retype_region_aligned_for_init[where sz = sz] - retype_region_obj_at[THEN hoare_vcg_const_imp_lift] - retype_region_caps_of[where sza = "\_. sz"] - | simp add:misc)+ - apply (rule_tac Q="\rv s. cte_wp_at (op \ cap.NullCap) (cref, oref) s \ post_retype_invs tp rv s - \ idle_thread s \ fst ` set slots - \ (\slot\set slots. - cte_wp_at (op = cap.NullCap) slot s) \ valid_etcbs s - \ untyped_is_device (transform_cap cap) = dev" + apply (simp add: vslot) + apply ((wp | simp add: mdb_cte_at_def | rule hoare_vcg_conj_lift, wps)+)[2] + apply (wp retype_region_aligned_for_init[where sz = sz] + retype_region_obj_at[THEN hoare_vcg_const_imp_lift] + retype_region_caps_of[where sza = "\_. sz"] + | simp add: misc)+ + apply (rule_tac Q="\rv s. cte_wp_at (op \ cap.NullCap) cref s + \ post_retype_invs tp rv s + \ idle_thread s \ fst ` set slots + \ untyped_is_device (transform_cap cap) = dev + \ (\slot\set slots. + cte_wp_at (op = cap.NullCap) slot s) \ valid_etcbs s" in hoare_post_imp) - apply (simp add:post_retype_invs_def split:split_if_asm) - apply ((clarsimp dest!:set_zip_leftD - simp:image_def invs_def valid_state_def valid_mdb_def - elim!:cte_wp_at_weakenE | intro conjI | drule (1) bspec | drule(1) mdb_cte_atD[rotated])+)[2] - apply (wp retype_region_cte_at_other'[where sz= sz] retype_region_post_retype_invs[where sz = sz] - hoare_vcg_const_Ball_lift retype_region_aligned_for_init) - apply (clarsimp simp:conj_comms misc cover) - apply (rule_tac Q="\r s. - cte_wp_at (op = (cap.UntypedCap dev (ptr && ~~ mask sz) - sz (unat ((ptr && mask sz) + (of_nat (length slots) << obj_bits_api tp us))))) (cref, oref) s \ - invs s \ valid_etcbs s \ pspace_no_overlap ptr sz s \ caps_no_overlap ptr sz s \ - region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s \ - caps_overlap_reserved {ptr..ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} s \ - idle_thread s \ fst ` set slots - \ cap_objects (transform_cap cap) = {ptr && ~~ mask sz..(ptr && ~~ mask sz) + (2 ^ sz - 1)} - \ (\x\set slots. cte_wp_at (op= cap.NullCap) x s) - \ untyped_is_device (transform_cap cap) = dev" - in hoare_strengthen_post[rotated]) - apply (clarsimp simp: invs_mdb invs_valid_pspace cte_wp_at_caps_of_state - split_paired_Ex) - apply (rule conjI,clarsimp) - apply (erule ranE) - apply (clarsimp simp: null_filter_def split: if_splits) - apply (frule_tac cap = capa in caps_of_state_ko[OF caps_of_state_valid]) - apply assumption - apply (elim disjE) - apply (clarsimp simp: cap_range_def is_cap_simps)+ - apply (rule disjointI) - apply clarsimp - apply (drule bspec,fastforce,clarsimp) - apply (drule_tac S = "{y}" in pspace_no_overlap_obj_range) - apply assumption - apply simp - apply (drule p_in_obj_range) - apply clarsimp+ - apply (intro exI conjI) - apply simp - apply simp - apply (clarsimp simp: cap_range_def blah p_assoc_help word_and_le2) - apply (rule_tac P = "cap = cap.UntypedCap dev (ptr && ~~ mask sz) sz idx" in hoare_gen_asm) - apply (simp add:bits_of_def region_in_kernel_window_def) - apply (rule hoare_vcg_conj_lift) - apply (rule hoare_strengthen_post[OF set_cap_sets]) - apply (clarsimp simp: cte_wp_at_caps_of_state shiftl_t2n field_simps) - apply (wp set_cap_no_overlap hoare_vcg_ball_lift - set_cap_free_index_invs_spec set_cap_caps_no_overlap - set_cap_cte_wp_at set_cap_descendants_range_in - set_untyped_cap_caps_overlap_reserved) + apply (simp add:post_retype_invs_def split:split_if_asm) + apply ((clarsimp dest!:set_zip_leftD + simp: vslot image_def invs_def valid_state_def valid_mdb_def cte_wp_at_caps_of_state + | intro conjI | drule (1) bspec | drule(1) mdb_cte_atD[rotated])+)[2] + apply (wp retype_region_cte_at_other'[where sz= sz] retype_region_post_retype_invs[where sz = sz] + hoare_vcg_const_Ball_lift retype_region_aligned_for_init) + apply (clarsimp simp:conj_comms misc cover) + apply (rule_tac Q="\r s. + cte_wp_at (\cp. \idx. cp = (cap.UntypedCap dev ptr' sz idx)) cref s \ + invs s \ pspace_no_overlap_range_cover ptr sz s \ caps_no_overlap ptr sz s \ + region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s \ + caps_overlap_reserved {ptr..ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} s \ + idle_thread s \ fst ` set slots + \ untyped_is_device (transform_cap cap) = dev + \ (\x\set slots. cte_wp_at (op= cap.NullCap) x s) \ valid_etcbs s" + in hoare_strengthen_post[rotated]) + apply (clarsimp simp: invs_mdb invs_valid_pspace cte_wp_at_caps_of_state + misc split_paired_Ex) + apply (rule conjI,clarsimp) + apply (erule ranE) + apply (clarsimp simp:null_filter_def split:if_splits) + apply (frule_tac cap = capa in caps_of_state_ko[OF caps_of_state_valid]) + apply assumption + apply (elim disjE) + apply (clarsimp simp:cap_range_def is_cap_simps)+ + apply (rule disjointI) + apply clarsimp + apply (drule bspec,fastforce,clarsimp) + apply (drule(1) pspace_no_overlap_obj_range) + apply (drule p_in_obj_range) + apply clarsimp+ + apply (auto simp: field_simps)[1] + apply (cases cref, simp, intro exI, rule conjI, assumption, + simp add: atLeastatMost_subset_iff word_and_le2 ptrs field_simps) + apply (rule_tac P="bits_of cap = sz" in hoare_gen_asm) + apply (simp add:bits_of_def) + apply (strengthen caps_region_kernel_window_imp[where p=cref] + invs_cap_refs_in_kernel_window)+ + apply (wp set_cap_no_overlap hoare_vcg_ball_lift + set_free_index_invs[where 'a=det_ext and + cap = "cap.UntypedCap dev (ptr && ~~ mask sz) sz (if reset then 0 else idx)", + simplified] + set_cap_cte_wp_at set_cap_descendants_range_in set_cap_caps_no_overlap + set_untyped_cap_caps_overlap_reserved set_cap_cte_cap_wp_to + hoare_vcg_ex_lift) + apply simp + apply wp + apply (simp split del: split_if) + apply (wp get_cap_wp) + apply (wp_once hoare_drop_imps) + apply wp + apply (rule validE_validE_R, rule_tac E="\\" and Q="\_. valid_etcbs and invs + and valid_untyped_inv_wcap untyped_invocation + (Some (cap.UntypedCap dev ptr' sz (if reset then 0 else idx))) and ct_active + and (\s. reset \ pspace_no_overlap {ptr' .. ptr' + 2 ^ sz - 1} s)" + in hoare_post_impErr) + apply (wp hoare_whenE_wp) + apply (rule validE_validE_R, rule hoare_post_impErr, rule reset_untyped_cap_invs_etc) + apply (clarsimp simp only: if_True simp_thms ptrs, intro conjI, assumption+) apply simp - apply simp - apply (wp get_cap_wp) + apply (clarsimp simp only: ui ptrs) + apply (frule(2) invoke_untyped_proofs.intro) + apply (clarsimp simp: ui cte_wp_at_caps_of_state bits_of_def + empty_descendants_range_in exI + free_index_of_def untyped_range_def + split_if[where P="\x. x \ unat v" for v] + split del: split_if) + apply (frule(1) valid_global_refsD2[OF _ invs_valid_global_refs]) + apply (strengthen refl subseteq_set_minus + free_range_of_untyped_subseteq' + range_le_free_range_of_untyped[mk_strg I E] + caps_region_kernel_window_imp[where p=cref])+ + apply (simp only: word_size word_bits_def[symmetric]) + apply (clarsimp simp: conj_comms invoke_untyped_proofs.simps + range_le_free_range_of_untyped + split_if[where P="\x. x \ unat v" for v] + split del: split_if) + apply (simp add: arg_cong[OF mask_out_sub_mask, where f="\y. x - y" for x] + field_simps invoke_untyped_proofs.idx_le_new_offs + invoke_untyped_proofs.idx_compare' + untyped_range_def invs_valid_idle invs_valid_pspace + is_aligned_neg_mask invoke_untyped_proofs.szw + free_range_of_untyped_pick_retype_addrs vslot + split del: split_if) + apply (clarsimp simp:detype_clear_um_independent conj_comms not_idle_thread_def + misc invs_valid_idle invs_valid_objs word_bits_def + atLeastatMost_subset_iff[where b=x and d=x for x] word_and_le2 + split del: split_if) + apply (clarsimp simp: range_cover.aligned bits_of_def field_simps + split del: split_if) + + apply (intro conjI) + apply (cases cref, fastforce dest: valid_idle_has_null_cap[rotated -1]) + apply (fastforce dest: ex_cte_cap_to_not_idle) + + apply (cases reset) + apply (simp, erule pspace_no_overlap_subset) + apply (simp add: atLeastatMost_subset_iff word_and_le2) + apply (clarsimp simp: field_simps dest!: invoke_untyped_proofs.ps_no_overlap) + + apply (auto dest: invoke_untyped_proofs.idx_le_new_offs)[1] + + apply (strengthen invoke_untyped_proofs.subset_stuff[THEN order_trans, mk_strg I E]) + apply (simp add: atLeastatMost_subset_iff word_and_le2) + + apply (drule invoke_untyped_proofs.usable_range_disjoint) + apply (clarsimp simp: field_simps mask_out_sub_mask shiftl_t2n) + + apply simp apply simp - using cte_at descendants_range misc invoke_untyped_proofs.cref_inv[OF pf] kernel_window_inv - invoke_untyped_proofs.idx_compare'[OF pf] invoke_untyped_proofs.usable_range_disjoint[OF pf] - cover invoke_untyped_proofs.vc[OF pf] subset_stuff - apply (clarsimp simp: invs_valid_idle invs_valid_pspace - cte_wp_at_caps_of_state bits_of_def shiftl_t2n - untyped_range.simps field_simps) - apply (intro conjI) - apply (simp add:range_cover.aligned) - apply (rule subset_trans[OF subset_stuff]) - apply (rule in_free_range) - apply simp - apply fastforce - apply (rule subseteq_set_minus) - apply (rule free_range_of_untyped_subseteq') - apply (rule idx_compare) - apply simp - apply (simp add: is_aligned_neg_mask) - apply (cut_tac range_cover.sz[OF cover],simp) - apply (drule free_range_of_untyped_pick_retype_addrs[OF _ vslot]) - apply (simp add: shiftl_t2n field_simps image_def) - apply (simp add: shiftl_t2n not_idle_thread_def field_simps range_cover_unat[OF cover]) - apply (rule idx_compare) - apply simp - apply (rule subset_trans[OF subset_stuff]) - apply (clarsimp simp: atLeastatMost_subset_iff word_and_le2) - apply (clarsimp dest!: slots_invD) - apply (drule ex_cte_cap_wp_to_not_idle) - apply (clarsimp simp: invs_valid_global_refs invs_valid_objs - invs_valid_idle invs_irq_node)+ - apply (simp add: not_idle_thread_def) - apply (clarsimp dest!: slots_invD) + apply (cut_tac vui1) + apply (clarsimp simp add: etc ptrs) + apply (clarsimp simp: ui cte_wp_at_caps_of_state valid_cap_simps + free_index_of_def) + apply auto done qed @@ -1860,46 +1803,30 @@ lemma decode_untyped_corres: apply (rule_tac r'=dc in corres_alternative_throw_splitE[rotated]) apply (simp add:liftE_bindE) apply (rule corres_symb_exec_r) - apply (clarsimp simp:corres_whenE_throwError_split_rhs corres_alternate2) + apply (clarsimp simp: corres_whenE_throwError_split_rhs corres_alternate2 + split del: split_if) apply (rule corres_alternate1) - apply (simp add:gets_get) + apply (simp add:gets_get split del: split_if) apply (rule corres_underlying_gets_pre_lhs) apply (rule_tac P' = "\s. valid_mdb s \ cte_at slot' s \ is_cnode_cap cnode_cap' \ cap_aligned cnode_cap' \ invs s \ not_idle_thread (obj_ref_of cnode_cap') s \ - free_index \ 2^sz \ is_aligned ptr sz \ sz < word_bits \ - (free_index = 0) = (descendants_of slot' (cdt s) ={} ) \ valid_etcbs s" + is_aligned ptr sz \ idx \ 2 ^ sz \ sz < word_bits \ + reset = (descendants_of slot' (cdt s) ={} ) \ valid_etcbs s" and P = "\s. s = x" in corres_returnOk) apply (simp add: translate_untyped_invocation_def transform_def get_free_ref_def) - apply (clarsimp simp: not_less) - apply (drule(4) range_cover_stuff) - apply (subst alignUp_plus) - apply (erule is_aligned_weaken) - apply (simp add:range_cover_def) apply (simp add:has_children_def KHeap_D.is_cdt_parent_def descendants_of_empty_lift word_neq_0_conv) - apply (subst alignUp_gt_0[where x = "2 ^ sz"]) - apply (rule is_aligned_weaken[where x = sz]) - apply (simp add:is_aligned_def) - apply (simp add:range_cover_def) - apply (simp add:range_cover_def) - apply (simp add: power_not_zero[where 'a=32, folded word_bits_def] range_cover_def) - apply (rule word_of_nat_le) - apply simp - apply (intro conjI) - apply (clarsimp simp:is_cap_simps cap_object_simps - transform_cslot_ptr_def bits_of_def - cap_aligned_def nat_bl_to_bin_nat_to_cref) - apply (subst of_nat_0) - apply (erule le_less_trans) - apply (clarsimp dest!:range_cover_sz_less') - apply simp - apply (wp check_free_index_wp) + apply (clarsimp simp: not_less is_cap_simps bits_of_def) + apply (clarsimp simp:is_cap_simps cap_object_simps + transform_cslot_ptr_def bits_of_def + cap_aligned_def nat_bl_to_bin_nat_to_cref) + apply (wp check_children_wp) apply simp apply (simp add:const_on_failure_def) apply clarsimp apply wp apply (clarsimp simp:conj_comms) - apply (wp mapME_x_inv_wp[OF hoare_pre(2)] | simp)+ + apply (wp mapME_x_inv_wp[OF hoare_pre(2)] | simp split del: split_if)+ apply (wp hoare_whenE_wp) apply (simp add:validE_def split del:if_splits) apply (rule_tac Q = "\r. op = s" in hoare_strengthen_post) @@ -1924,8 +1851,7 @@ lemma decode_untyped_corres: transform_cslot_ptr_def bits_of_def cap_aligned_def nat_bl_to_bin_nat_to_cref) apply simp - apply (clarsimp,intro conjI impI allI) - apply ((fastforce simp:invs_valid_idle)+)[5] (* sseefried; Brittle proof. Change number? *) + apply clarsimp apply (rule hoare_pre) apply (wp hoare_drop_imp | simp)+ apply fastforce @@ -1950,16 +1876,6 @@ lemma decode_untyped_corres: apply (frule(1) caps_of_state_valid) apply (rule ccontr) apply (clarsimp simp:valid_cap_simps cap_aligned_def) - apply (frule cte_wp_at_caps_descendants_range_inI[where ptr = ptr and cref = slot' and sz = sz]) - apply (clarsimp simp:cte_wp_at_caps_of_state is_aligned_neg_mask_eq) - apply simp+ - apply (simp add:is_aligned_neg_mask_eq) - apply (drule descendants_range_imply_no_descendants[rotated 3]) - apply clarsimp+ - apply (clarsimp simp:descendants_range_def2) - apply (clarsimp dest!:invs_mdb simp:valid_mdb_def) - apply simp - apply simp apply (rule hoare_pre,wp,simp) apply (wp hoare_drop_imp mapME_x_inv_wp2 | simp add:whenE_def split del:split_if)+ apply (rule hoare_pre,wp,simp) diff --git a/proof/infoflow/ADT_IF.thy b/proof/infoflow/ADT_IF.thy index 1d80956f1..decd2abbf 100644 --- a/proof/infoflow/ADT_IF.thy +++ b/proof/infoflow/ADT_IF.thy @@ -3047,6 +3047,34 @@ lemma irq_state_inv_trivE': apply simp done +crunch irq_state_of_state[wp]: init_arch_objects "\s. P (irq_state_of_state s)" + (wp: crunch_wps dmo_wp ignore: do_machine_op) + +lemma reset_untyped_cap_irq_state_inv: + "\irq_state_inv st and K (irq_is_recurring irq st)\ + reset_untyped_cap slot \\y. irq_state_inv st\, \\y. irq_state_next st\" + apply (cases "irq_is_recurring irq st", simp_all) + apply (simp add: reset_untyped_cap_def) + apply (rule hoare_pre) + apply (wp no_irq_clearMemory mapME_x_wp' + hoare_vcg_const_imp_lift + preemption_point_irq_state_inv'[where irq=irq] + | rule irq_state_inv_triv + | simp + | wp_once dmo_wp)+ + done + +lemma invoke_untyped_irq_state_inv: + "\irq_state_inv st and K (irq_is_recurring irq st)\ + invoke_untyped ui \\y. irq_state_inv st\, \\y. irq_state_next st\" + apply (cases ui, simp add: invoke_untyped_def mapM_x_def[symmetric]) + apply (rule hoare_pre) + apply (wp mapM_x_wp' hoare_whenE_wp + reset_untyped_cap_irq_state_inv[where irq=irq] + | rule irq_state_inv_triv + | simp)+ + done + lemma perform_invocation_irq_state_inv: "\irq_state_inv st and (\s. \blah. @@ -3060,7 +3088,7 @@ lemma perform_invocation_irq_state_inv: perform_invocation x y oper \\_. irq_state_inv st\, \\_. irq_state_next st\" apply(case_tac oper) apply(simp | wp)+ - apply((wp irq_state_inv_triv | simp)+)[4] + apply((wp invoke_untyped_irq_state_inv[where irq=irq] irq_state_inv_triv | simp)+)[4] apply((wp invoke_tcb_irq_state_inv invoke_cnode_irq_state_inv[simplified validE_R_def] | simp add: invoke_domain_def |blast)+)[5] apply (rule hoare_validE_cases) apply(rule hoare_post_impErr[OF valid_validE]) diff --git a/proof/infoflow/Arch_IF.thy b/proof/infoflow/Arch_IF.thy index e92585a68..5fed7d99a 100644 --- a/proof/infoflow/Arch_IF.thy +++ b/proof/infoflow/Arch_IF.thy @@ -70,9 +70,11 @@ lemma detype_irq_state_of_state[simp]: apply(simp add: detype_def) done -crunch irq_state_of_state[wp]: invoke_untyped "\s. P (irq_state_of_state s)" - (wp: dmo_wp modify_wp hoare_unless_wp crunch_wps simp: crunch_simps - ignore: freeMemory simp: freeMemory_def storeWord_def clearMemory_def machine_op_lift_def machine_rest_lift_def mapM_x_defsym) +text {* Not true of invoke_untyped any more. *} +crunch irq_state_of_state[wp]: retype_region,create_cap,delete_objects "\s. P (irq_state_of_state s)" + (wp: dmo_wp modify_wp crunch_wps + simp: crunch_simps ignore: freeMemory + simp: freeMemory_def storeWord_def clearMemory_def machine_op_lift_def machine_rest_lift_def mapM_x_defsym) crunch irq_state_of_state[wp]: invoke_irq_control "\s. P (irq_state_of_state s)" @@ -2184,7 +2186,7 @@ lemma perform_asid_control_invocation_globals_equiv: word1 \ idle_thread b \ (\ idx. cte_wp_at (op = (UntypedCap False word1 pageBits idx)) cslot_ptr2 b) \ descendants_of cslot_ptr2 (cdt b) = {} \ - pspace_no_overlap word1 pageBits b" + pspace_no_overlap_range_cover word1 pageBits b" in hoare_strengthen_post) prefer 2 apply (clarsimp simp: globals_equiv_def invs_valid_global_objs) @@ -2194,22 +2196,22 @@ lemma perform_asid_control_invocation_globals_equiv: apply (rule conjI, fastforce simp: cte_wp_at_def) apply (clarsimp simp: obj_bits_api_def default_arch_object_def) apply (frule untyped_cap_aligned, simp add: invs_valid_objs) + apply (clarsimp simp: cte_wp_at_caps_of_state) + apply (strengthen refl caps_region_kernel_window_imp[mk_strg I E]) + apply (simp add: invs_valid_objs invs_cap_refs_in_kernel_window + atLeastatMost_subset_iff word_and_le2 + is_aligned_neg_mask_eq) apply(rule conjI, rule descendants_range_caps_no_overlapI) apply assumption - apply(simp add: is_aligned_neg_mask_eq) + apply(simp add: is_aligned_neg_mask_eq cte_wp_at_caps_of_state) apply(simp add: is_aligned_neg_mask_eq empty_descendants_range_in) - apply(rule conjI, drule cap_refs_in_kernel_windowD2) - apply(simp add: invs_cap_refs_in_kernel_window) - apply(fastforce simp: cap_range_def is_aligned_neg_mask_eq) apply(clarsimp simp: range_cover_def) apply(subst is_aligned_neg_mask_eq[THEN sym], assumption) apply(simp add: mask_neg_mask_is_zero pageBits_def) - apply (rule conjI) - apply (rule free_index_of_UntypedCap[symmetric]) - apply (simp add: invs_valid_objs) - apply(wp delete_objects_invs_ex[where dev=False] delete_objects_pspace_no_overlap[where dev=False] + apply(wp add: delete_objects_invs_ex[where dev=False] delete_objects_pspace_no_overlap[where dev=False] delete_objects_globals_equiv delete_objects_valid_ko_at_arm hoare_vcg_ex_lift + del: Untyped_AI.delete_objects_pspace_no_overlap | simp add: page_bits_def)+ apply (clarsimp simp: conj_comms invs_valid_ko_at_arm invs_psp_aligned invs_valid_objs valid_aci_def) apply (clarsimp simp: cte_wp_at_caps_of_state) diff --git a/proof/infoflow/Decode_IF.thy b/proof/infoflow/Decode_IF.thy index 44b690faa..f466e8746 100644 --- a/proof/infoflow/Decode_IF.thy +++ b/proof/infoflow/Decode_IF.thy @@ -25,8 +25,7 @@ lemma data_to_obj_type_rev: lemma ensure_empty_rev: "reads_equiv_valid_inv A aag (K (is_subject aag (fst slot))) (ensure_empty slot)" unfolding ensure_empty_def fun_app_def - apply (wp get_cap_rev) - apply simp + apply (wp get_cap_rev | simp)+ done @@ -116,11 +115,14 @@ lemma decode_cnode_invocation_rev: unfolding decode_cnode_invocation_def fun_app_def apply (rule equiv_valid_guard_imp) apply (simp add: unlessE_whenE) - apply (wp if_apply_ev derive_cap_rev whenE_inv hoare_vcg_imp_lift_R + apply wp + apply ((wp if_apply_ev derive_cap_rev whenE_inv hoare_vcg_imp_lift_R lookup_slot_for_cnode_op_rev hoare_vcg_all_lift_R lookup_slot_for_cnode_op_authorised ensure_empty_rev get_cap_rev | simp add: split_def unlessE_whenE split del: split_if - | wpc)+ + del: hoare_True_E_R + | wpc + | (wp_once hoare_drop_imps, wp_once lookup_slot_for_cnode_op_authorised))+) apply(auto dest: bspec[where x="excaps ! 0"] bspec[where x="excaps ! Suc 0"] intro: nth_mem elim: prop_of_obj_ref_of_cnode_cap dest!: is_cnode_into_is_subject simp: expand_len_gr_Suc_0) @@ -129,7 +131,9 @@ lemma decode_cnode_invocation_rev: lemma range_check_ev: "equiv_valid_inv I A \ (range_check v v_min v_max)" unfolding range_check_def fun_app_def unlessE_whenE - apply wp + apply (rule equiv_valid_guard_imp) + apply wp + apply simp done @@ -202,7 +206,7 @@ lemma OR_choice_def2: "(\P. \P\ (c :: bool det_ext_monad) \ lemma check_prio_rev: "reads_respects aag l (is_subject aag \ cur_thread) (check_prio prio)" apply (clarsimp simp: check_prio_def) - apply (wp thread_get_reads_respects) + apply (wp thread_get_reads_respects hoare_drop_imps) by (clarsimp simp: reads_equiv_def) lemma decode_set_priority_rev: diff --git a/proof/infoflow/FinalCaps.thy b/proof/infoflow/FinalCaps.thy index b4b9be8b8..a9e378729 100644 --- a/proof/infoflow/FinalCaps.thy +++ b/proof/infoflow/FinalCaps.thy @@ -2088,80 +2088,114 @@ lemma delete_objects_silc_inv: apply (wp detype_silc_inv | simp add: ptr_range_def)+ done -(* yet another horrendous invoke_untyped proof -- TODO: clean me up *) +lemma set_cap_silc_inv_simple: + "\ silc_inv aag st and cte_wp_at (\cp. cap_irqs cp = cap_irqs cap + \ Structures_A.obj_refs cp = Structures_A.obj_refs cap) slot + and K (is_subject aag (fst slot))\ + set_cap cap slot + \\_. silc_inv aag st\" + apply (wp set_cap_silc_inv) + apply (clarsimp simp: cte_wp_at_caps_of_state) + apply (rule conjI; clarsimp) + apply (drule caps_of_state_cteD) + apply (frule(1) silc_invD) + apply (clarsimp simp: intra_label_cap_def) + apply (rule exI, rule conjI, assumption) + apply (simp add: cap_points_to_label_def) + apply (simp add: slots_holding_overlapping_caps_def) + apply (simp add: silc_inv_def) + done + +lemma reset_untyped_cap_silc_inv: + "\ silc_inv aag st and cte_wp_at is_untyped_cap slot + and invs and pas_refined aag + and (\s. descendants_of slot (cdt s) = {}) + and K (is_subject aag (fst slot))\ + reset_untyped_cap slot + \\_. silc_inv aag st\" + apply (rule hoare_gen_asm) + apply (simp add: reset_untyped_cap_def) + apply (wp set_cap_silc_inv_simple | simp add: unless_def)+ + apply (rule valid_validE, rule_tac Q="\_. cte_wp_at is_untyped_cap slot + and silc_inv aag st" in hoare_strengthen_post) + apply (rule validE_valid, rule mapME_x_inv_wp, rule hoare_pre) + apply (wp mapME_x_inv_wp preemption_point_inv set_cap_cte_wp_at + set_cap_silc_inv_simple | simp)+ + apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps) + apply simp + apply (wp hoare_vcg_const_imp_lift delete_objects_silc_inv get_cap_wp | simp)+ + apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def) + apply (frule(1) cap_auth_caps_of_state) + apply (clarsimp simp: aag_cap_auth_def aag_has_Control_iff_owns + ptr_range_def[symmetric]) + apply (frule if_unsafe_then_capD[OF caps_of_state_cteD], clarsimp+) + apply (drule ex_cte_cap_protects[OF _ _ _ _ order_refl], erule caps_of_state_cteD) + apply (clarsimp simp: descendants_range_def2 empty_descendants_range_in) + apply clarsimp+ + done + +lemma reset_untyped_cap_untyped_cap: + "\cte_wp_at (\cp. is_untyped_cap cp \ P True (untyped_range cp)) slot + and invs + and (\s. descendants_of slot (cdt s) = {})\ + reset_untyped_cap slot + \\rv. cte_wp_at (\cp. P (is_untyped_cap cp) (untyped_range cp)) slot\" + apply (simp add: reset_untyped_cap_def) + apply (rule hoare_pre) + apply (wp set_cap_cte_wp_at | simp add: unless_def)+ + apply (rule valid_validE, rule_tac Q="\rv. cte_wp_at (\cp. is_untyped_cap cp + \ is_untyped_cap cap + \ untyped_range cp = untyped_range cap + \ P True (untyped_range cp)) slot" + in hoare_strengthen_post) + apply (wp mapME_x_inv_wp preemption_point_inv set_cap_cte_wp_at + | simp | clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def + ptr_range_def[symmetric])+ + apply (wp get_cap_wp) + apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps ptr_range_def[symmetric]) + apply (frule if_unsafe_then_capD[OF caps_of_state_cteD], clarsimp+) + apply (drule ex_cte_cap_protects[OF _ _ _ _ order_refl], erule caps_of_state_cteD) + apply (clarsimp simp: descendants_range_def2 empty_descendants_range_in) + apply clarsimp+ + done + lemma invoke_untyped_silc_inv: - "\ silc_inv aag st and authorised_untyped_inv_state aag ui and valid_untyped_inv ui and - K (authorised_untyped_inv aag ui)\ + "\ silc_inv aag st and invs and pas_refined aag + and ct_active and valid_untyped_inv ui + and K (authorised_untyped_inv aag ui)\ invoke_untyped ui \ \_. silc_inv aag st \" apply(rule hoare_gen_asm) - apply(case_tac ui, simp add: mapM_x_def[symmetric] authorised_untyped_inv_def) - apply(rename_tac word1 word2 apiobjt nat list dev) - apply wp - apply(rule_tac Q="\ r s. silc_inv aag st s \ (\ x\set list. is_subject aag (fst x)) \ (\ oref\set orefs. is_subject aag oref)" in hoare_strengthen_post) - apply (wp mapM_x_wp[OF _ subset_refl] create_cap_silc_inv retype_region_silc_inv - retype_region_ret_is_subject[simplified] set_cap_silc_inv - slots_holding_overlapping_caps_from_silc_inv[where aag=aag and st=st] - hoare_vcg_ex_lift delete_objects_silc_inv get_cap_wp static_imp_wp - | erule in_set_zipE - | clarsimp simp: split_paired_Ball - | blast )+ - apply(intro allI impI conjI) - apply(simp add: valid_untyped_inv_def) - apply(drule (1) silc_invD) - apply(fastforce simp: intra_label_cap_def cap_points_to_label_def) - apply(elim exE, rename_tac lslot) - apply(rule_tac x="fst lslot" in exI, simp add: authorised_untyped_inv_state_def) - apply(rule_tac x="snd lslot" in exI) - apply(drule (1) cte_wp_at_eqD2) - apply(simp add: bits_of_def) - apply(elim conjE) - apply(rule subst[rotated, OF _ slots_holding_overlapping_caps_eq]) - apply assumption - apply simp - apply simp - apply(fastforce simp: authorised_untyped_inv_state_def dest: cte_wp_at_eqD2) - apply(fastforce simp: silc_inv_def) - apply(drule (1) cte_wp_at_eqD2, simp) - apply(subst (asm) bits_of_UntypedCap[symmetric], assumption) - apply(drule (1) cte_wp_at_eqD2, clarsimp simp: authorised_untyped_inv_state_def bits_of_UntypedCap ptr_range_def cte_wp_at_sym p_assoc_help) - apply(drule (1) cte_wp_at_eqD2, simp) - apply(subst (asm) bits_of_UntypedCap[symmetric], assumption) - apply(drule (1) cte_wp_at_eqD2, clarsimp simp: authorised_untyped_inv_state_def bits_of_UntypedCap ptr_range_def cte_wp_at_sym p_assoc_help) - apply(drule (1) silc_invD) - apply(fastforce simp: intra_label_cap_def cap_points_to_label_def) - apply(elim exE, rename_tac lslot) - apply(rule_tac x="fst lslot" in exI, simp) - apply(rule_tac x="snd lslot" in exI) - apply(drule (1) cte_wp_at_eqD2) - apply(simp add: bits_of_def) - apply(elim conjE) - apply(rule subst[rotated, OF _ slots_holding_overlapping_caps_eq]) - apply assumption - apply simp - apply simp - apply(fastforce simp: silc_inv_def) - apply(simp add: cte_wp_at_sym) - apply(drule (1) cte_wp_at_eqD2) - apply(simp add: bits_of_UntypedCap) - apply(simp add: cte_wp_at_sym) - apply(drule (1) cte_wp_at_eqD2) - apply(clarsimp simp: bits_of_UntypedCap ptr_range_def authorised_untyped_inv_state_def word_and_le2 p_assoc_help word_and_le1) - apply(drule spec, erule impE, assumption) - apply(simp add: bits_of_UntypedCap) - apply(drule_tac y=word2 in order_trans[rotated]) - apply(rule word_and_le2) - apply fastforce - apply(drule (1) cte_wp_at_eqD2, simp) - apply(subst (asm) bits_of_UntypedCap[symmetric], assumption) - apply(simp add: cte_wp_at_sym) - apply(drule (1) cte_wp_at_eqD2) - apply(clarsimp simp: bits_of_UntypedCap ptr_range_def authorised_untyped_inv_state_def p_assoc_help) - apply(drule spec, erule impE, assumption) - apply(simp add: bits_of_UntypedCap) - apply(drule_tac y=word2 in order_trans[rotated]) - apply(rule word_and_le2) - by fastforce + apply (rule hoare_pre) + apply (rule_tac Q="\_. silc_inv aag st + and cte_wp_at (\cp. is_untyped_cap cp \ (\x \ untyped_range cp. + is_subject aag x)) (case ui of Invocations_A.Retype src_slot _ _ _ _ _ _ _ \ + src_slot)" in hoare_strengthen_post) + apply (rule invoke_untyped_Q) + apply (rule hoare_pre, wp create_cap_silc_inv create_cap_pas_refined) + apply (clarsimp simp: authorised_untyped_inv_def) + apply (auto simp: cte_wp_at_caps_of_state)[1] + apply ((wp | simp)+)[1] + apply (rule hoare_pre) + apply (wp retype_region_silc_inv retype_cte_wp_at | simp)+ + apply clarsimp + apply (strengthen range_cover_le[mk_strg I E]) + apply (clarsimp simp: cte_wp_at_caps_of_state) + apply (simp add: invs_valid_pspace) + apply (erule ball_subset) + apply (simp add: word_and_le2 field_simps) + apply (rule hoare_pre) + apply (wp set_cap_silc_inv_simple set_cap_cte_wp_at) + apply (cases ui, clarsimp simp: cte_wp_at_caps_of_state is_cap_simps + split del: split_if cong: if_cong) + apply (clarsimp simp: authorised_untyped_inv_def) + apply (wp reset_untyped_cap_silc_inv reset_untyped_cap_untyped_cap) + apply simp + apply (cases ui, clarsimp simp: cte_wp_at_caps_of_state + authorised_untyped_inv_def) + apply (frule(1) cap_auth_caps_of_state) + apply (clarsimp simp: aag_cap_auth_def aag_has_Control_iff_owns) + done lemma perform_page_table_invocation_silc_ionv_get_cap_helper: "\silc_inv aag st and cte_wp_at (is_pt_cap or is_pg_cap) xa\ @@ -3166,4 +3200,4 @@ lemma call_kernel_silc_inv: end -end \ No newline at end of file +end diff --git a/proof/infoflow/IRQMasks_IF.thy b/proof/infoflow/IRQMasks_IF.thy index e1b5fbc33..f72ea8eeb 100644 --- a/proof/infoflow/IRQMasks_IF.thy +++ b/proof/infoflow/IRQMasks_IF.thy @@ -40,10 +40,11 @@ lemma delete_objects_irq_masks[wp]: apply(wp dmo_wp no_irq_mapM_x no_irq | simp add: freeMemory_def no_irq_storeWord)+ done - crunch irq_masks[wp]: invoke_untyped "\s. P (irq_masks_of_state s)" - (ignore: delete_objects wp: hoare_unless_wp - crunch_wps dmo_wp no_irq simp: crunch_simps no_irq_clearMemory no_irq_cleanCacheRange_PoU mapM_x_def_bak) + (ignore: delete_objects wp: crunch_wps dmo_wp + wp: mapME_x_inv_wp preemption_point_inv + simp: crunch_simps no_irq_clearMemory no_irq_cleanCacheRange_PoU + mapM_x_def_bak unless_def) crunch irq_masks[wp]: cap_insert "\s. P (irq_masks_of_state s)" (wp: crunch_wps) diff --git a/proof/infoflow/PasUpdates.thy b/proof/infoflow/PasUpdates.thy index b39d17577..027a692fe 100644 --- a/proof/infoflow/PasUpdates.thy +++ b/proof/infoflow/PasUpdates.thy @@ -60,9 +60,10 @@ lemma invoke_cnode_domain_fields[wp]: "\domain_fields P\ invoke_ apply (wp | wpc | clarsimp simp: without_preemption_def crunch_simps | intro impI conjI | wp_once hoare_drop_imps hoare_vcg_all_lift)+ done -crunch domain_fields[wp]: set_domain,set_priority,switch_if_required_to,set_extra_badge,attempt_switch_to,handle_send,handle_recv,handle_reply "domain_fields P" (wp: syscall_valid crunch_wps rec_del_preservation cap_revoke_preservation transfer_caps_loop_pres simp: crunch_simps check_cap_at_def filterM_mapM unless_def detype_def detype_ext_def mapM_x_defsym ignore: without_preemption filterM rec_del check_cap_at cap_revoke resetTimer ackInterrupt getFAR getDFSR getIFSR getActiveIRQ const_on_failure freeMemory) - - +crunch domain_fields[wp]: set_domain,set_priority,switch_if_required_to,set_extra_badge,attempt_switch_to,handle_send,handle_recv,handle_reply "domain_fields P" + (wp: syscall_valid crunch_wps rec_del_preservation cap_revoke_preservation + transfer_caps_loop_pres mapME_x_inv_wp + simp: crunch_simps check_cap_at_def filterM_mapM unless_def detype_def detype_ext_def mapM_x_defsym ignore: without_preemption filterM rec_del check_cap_at cap_revoke resetTimer ackInterrupt getFAR getDFSR getIFSR getActiveIRQ const_on_failure freeMemory) crunch cur_domain[wp]: transfer_caps_loop, ethread_set, thread_set_priority, set_priority, set_domain, invoke_domain, cap_move_ext, recycle_cap_ext,timer_tick, diff --git a/proof/infoflow/Retype_IF.thy b/proof/infoflow/Retype_IF.thy index a12630ddd..985707264 100644 --- a/proof/infoflow/Retype_IF.thy +++ b/proof/infoflow/Retype_IF.thy @@ -541,84 +541,31 @@ lemma do_machine_op_mapM_x: apply(clarsimp simp: mapM_x_Cons do_machine_op_bind[OF ef empty_fail_mapM_x[OF ef]]) done -lemma create_word_objects_reads_respects: - "reads_respects aag l \ (create_word_objects ptr bits sz dev)" - unfolding create_word_objects_def fun_app_def reserve_region_def - apply(subst do_machine_op_mapM_x[OF empty_fail_clearMemory]) - apply(wp dmo_clearMemory_reads_respects mapM_x_ev hoare_unless_wp +text {* + | simp add: unless_def when_def | intro conjI impI)+ - done - -lemma create_word_objects_globals_equiv: - notes blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff - shows - "\ globals_equiv s and (\ s. range_cover ptr sz bits numObjects \ - (0::word32) < of_nat numObjects \ 2 \ bits \ {ptr..ptr + of_nat numObjects * 2 ^ bits - 1} \ range_of_arm_globals_frame s = {})\ - create_word_objects ptr numObjects bits dev - \ \_. globals_equiv s \" - unfolding create_word_objects_def reserve_region_def fun_app_def do_machine_op_def - apply(rule hoare_pre) - apply(simp add: do_machine_op_def clearMemory_def split_def cleanCacheRange_PoU_def) - apply(wp hoare_unless_wp) - apply clarsimp - apply(erule use_valid) - apply(wp mapM_x_wp' storeWord_globals_equiv mol_globals_equiv | simp add: cleanByVA_PoU_def)+ - apply(simp_all) - apply(drule ptr_range_subset[rotated]) - apply (simp add: range_cover_def[where 'a=32, folded word_bits_def])+ - apply (fastforce intro: is_aligned_add is_aligned_shiftl_self) - apply(erule disjoint_subset) - apply(erule disjoint_subset[rotated]) - apply(clarsimp del: subsetI simp: shiftl_t2n ptr_range_def) - apply(drule_tac p="unat n" in range_cover_subset) - apply(rule unat_less_helper) - apply(rule minus_one_helper5) - apply simp - apply assumption - apply(fastforce dest: unat_less_helper) - apply(clarsimp simp: mult.commute) - done - -lemma create_word_objects_reads_respects_g: - "reads_respects_g aag l (\ s. range_cover ptr sz bits numObjects \ - (0::word32) < of_nat numObjects \ 2 \ bits \ {ptr..ptr + of_nat numObjects * 2 ^ bits - 1} \ range_of_arm_globals_frame s = {}) (create_word_objects ptr numObjects bits dev)" - apply(rule equiv_valid_guard_imp) - apply(rule reads_respects_g) - apply(rule create_word_objects_reads_respects) - apply(rule doesnt_touch_globalsI[OF create_word_objects_globals_equiv]) - apply auto - done +*} crunch arm_global_pd: copy_global_mappings "\ s. P (arm_global_pd (arch_state s))" (wp: crunch_wps simp: crunch_simps) -definition word_object_range_cover_globals where - "word_object_range_cover_globals new_type ptr sz num_objects s \ - if new_type - \ ArchObject ` {SmallPageObj, LargePageObj, SectionObj, SuperSectionObj} - then range_cover ptr sz (word_object_size new_type) num_objects \ - ({ptr..ptr + of_nat num_objects * 2 ^ word_object_size new_type - 1} \ - range_of_arm_globals_frame s = {}) - else True" - lemma init_arch_objects_reads_respects_g: "reads_respects_g aag l ((\ s. arm_global_pd (arch_state s) \ set refs \ pspace_aligned s \ valid_arch_state s) and - word_object_range_cover_globals new_type ptr sz num_objects and K (\x\set refs. is_subject aag x) and K (\x\set refs. new_type = ArchObject PageDirectoryObj \ is_aligned x pd_bits) and K ((0::word32) < of_nat num_objects)) - (init_arch_objects new_type ptr num_objects obj_sz refs dev)" + (init_arch_objects new_type ptr num_objects obj_sz refs)" apply(unfold init_arch_objects_def fun_app_def) apply(rule gen_asm_ev)+ apply(subst do_machine_op_mapM_x[OF empty_fail_cleanCacheRange_PoU])+ apply(rule equiv_valid_guard_imp) - apply(wp create_word_objects_reads_respects_g dmo_cleanCacheRange_reads_respects_g mapM_x_ev'' equiv_valid_guard_imp[OF copy_global_mappings_reads_respects_g] copy_global_mappings_valid_arch_state copy_global_mappings_pspace_aligned copy_global_mappings_arm_global_pd hoare_vcg_ball_lift | wpc | simp)+ - apply(fastforce simp: word_object_range_cover_globals_def word_object_size_def) + apply(wp dmo_cleanCacheRange_reads_respects_g mapM_x_ev'' equiv_valid_guard_imp[OF copy_global_mappings_reads_respects_g] copy_global_mappings_valid_arch_state copy_global_mappings_pspace_aligned copy_global_mappings_arm_global_pd hoare_vcg_ball_lift | wpc | simp)+ + apply(fastforce simp: word_object_size_def) done lemma copy_global_mappings_globals_equiv: @@ -634,25 +581,24 @@ lemma copy_global_mappings_globals_equiv: apply(simp_all) done - lemma init_arch_objects_globals_equiv: "\ globals_equiv s and (\ s. arm_global_pd (arch_state s) \ set refs \ pspace_aligned s \ valid_arch_state s) and - word_object_range_cover_globals new_type ptr sz num_objects and - K (\x\set refs. new_type = ArchObject PageDirectoryObj - \ is_aligned x pd_bits) and - K ((0::word32) < of_nat num_objects)\ - (init_arch_objects new_type ptr num_objects obj_sz refs dev) + K (\x\set refs. is_aligned x (obj_bits_api new_type obj_sz))\ + (init_arch_objects new_type ptr num_objects obj_sz refs) \ \_. globals_equiv s \" unfolding init_arch_objects_def fun_app_def apply(rule hoare_gen_asm)+ apply(subst do_machine_op_mapM_x[OF empty_fail_cleanCacheRange_PoU])+ apply(rule hoare_pre) - apply(wpc | wp create_word_objects_globals_equiv mapM_x_wp[OF dmo_cleanCacheRange_PoU_globals_equiv subset_refl])+ + apply(wpc | wp mapM_x_wp[OF dmo_cleanCacheRange_PoU_globals_equiv subset_refl])+ apply(rule_tac Q="\_. globals_equiv s and (\ s. arm_global_pd (arch_state s) \ set refs)" in hoare_strengthen_post) - apply(wp mapM_x_wp[OF _ subset_refl] copy_global_mappings_globals_equiv copy_global_mappings_arm_global_pd copy_global_mappings_arm_globals_frame dmo_cleanCacheRange_PoU_globals_equiv | simp | blast)+ - apply (fastforce simp: word_object_range_cover_globals_def word_object_size_def) + apply(wp mapM_x_wp[OF _ subset_refl] copy_global_mappings_globals_equiv + copy_global_mappings_arm_global_pd copy_global_mappings_arm_globals_frame + dmo_cleanCacheRange_PoU_globals_equiv + | simp add: obj_bits_api_def default_arch_object_def + pd_bits_def pageBits_def | blast)+ done lemma create_cap_reads_respects_g: @@ -722,7 +668,7 @@ lemma retype_region_globals_equiv: (\s. \idx. cte_wp_at (\c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \ (idx \ unat (ptr && mask sz) \ - pspace_no_overlap ptr sz s)) and + pspace_no_overlap_range_cover ptr sz s)) and invs and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects) and K (0 < num_objects)\ @@ -735,7 +681,7 @@ lemma retype_region_globals_equiv: apply clarsimp apply (simp only: globals_equiv_def) apply (clarsimp split del: split_if) - apply (subgoal_tac "pspace_no_overlap ptr sz sa") + apply (subgoal_tac "pspace_no_overlap_range_cover ptr sz sa") apply (rule conjI) apply(clarsimp simp: pspace_no_overlap_def) apply(drule_tac x="arm_global_pd (arch_state sa)" in spec) @@ -798,7 +744,7 @@ lemma retype_region_reads_respects_g: ((\s. \idx. cte_wp_at (\c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \ (idx \ unat (ptr && mask sz) \ - pspace_no_overlap ptr sz s)) and + pspace_no_overlap_range_cover ptr sz s)) and invs and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects) and K (0 < num_objects)) @@ -868,7 +814,6 @@ lemma detype_globals_equiv: apply(wp) apply(clarsimp simp: globals_equiv_def detype_def idle_equiv_def tcb_at_def2) done - lemma detype_reads_respects_g: "reads_respects_g aag l ((\ s. arm_global_pd (arch_state s) \ S) and (\s. idle_thread s \ S)) (modify (detype S))" apply (rule equiv_valid_guard_imp) @@ -1010,22 +955,6 @@ lemma delete_objects_reads_respects_g: apply simp done -lemma word_object_range_cover_globals_inv: - assumes agpd: - "\ P. \ \ s. P (arm_globals_frame (arch_state s)) \ - f - \ \ rv s. P (arm_globals_frame (arch_state s)) \" - shows - "\ word_object_range_cover_globals new_type ptr sz num_objects \ f - \\_. word_object_range_cover_globals new_type ptr sz num_objects\" - apply(clarsimp simp: valid_def word_object_range_cover_globals_def split_def) - apply safe - apply(drule use_valid | - rule_tac P="\ y. {ptr..ptr + of_nat num_objects * 2 ^ sz - 1} \ ptr_range y 12 = {}" - for sz in agpd | fastforce)+ - done - - lemma set_cap_reads_respects_g: "reads_respects_g aag l (valid_global_objs and K (is_subject aag (fst slot))) (set_cap cap slot)" apply(rule equiv_valid_guard_imp) @@ -1033,31 +962,6 @@ lemma set_cap_reads_respects_g: apply(rule doesnt_touch_globalsI[OF set_cap_globals_equiv]) by simp -(* FIXME: put this into Retype_AC instead *) -lemma set_free_index_invs': - "\ (\s. invs s \ - cte_wp_at (op = cap) slot s \ - (free_index_of cap \ idx' \ - (descendants_range_in {word1..word1 + 2 ^ sz - 1} slot s \ - pspace_no_overlap word1 sz s)) \ - idx' \ 2 ^ sz \ - is_untyped_cap cap) and - K(word1 = obj_ref_of cap \ sz = bits_of cap \ dev = cap_is_device cap)\ - set_cap - (UntypedCap dev word1 sz idx') - slot - \\_. invs \" - apply(rule hoare_gen_asm) - apply(case_tac cap, simp_all add: bits_of_def) - apply(case_tac "free_index_of cap \ idx'") - apply simp - apply(cut_tac cap=cap and cref=slot and idx="idx'" in set_free_index_invs) - apply(simp add: free_index_update_def conj_comms) - apply simp - apply(wp set_untyped_cap_invs_simple | simp)+ - apply(fastforce simp: cte_wp_at_def) - done - (*FIXME move*) lemma when_ev: "\C \ equiv_valid I A A P handle\ \ @@ -1092,50 +996,207 @@ lemma get_cap_reads_respects_g: apply simp done +lemma irq_state_independent_globals_equiv[simp]: + "irq_state_independent_A (globals_equiv st)" + by (clarsimp simp: irq_state_independent_A_def globals_equiv_def + idle_equiv_def) -lemma word_object_range_cover_globalsI: - notes blah[simp del] = untyped_range.simps usable_untyped_range.simps atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff - shows - "\range_cover ptr sz (obj_bits_api new_type us) num_objects; - cte_wp_at (op = (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s; invs s; - num_objects \ 0\ \ - word_object_range_cover_globals new_type ptr sz num_objects s" - apply(clarsimp simp: word_object_range_cover_globals_def obj_bits_api_def word_object_size_def default_arch_object_def) - apply(frule range_cover_subset', simp+) - apply(frule untyped_caps_do_not_overlap_arm_globals_frame, (simp add: invs_valid_objs invs_arch_state invs_valid_global_refs)+) - apply(clarsimp split: apiobject_type.splits aobject_type.splits simp: default_arch_object_def) - apply(erule disjoint_subset) - apply(erule disjoint_subset[rotated]) - apply(simp add: ptr_range_def blah word_and_le2) - apply(erule disjoint_subset) - apply(erule disjoint_subset[rotated]) - apply(simp add: ptr_range_def blah word_and_le2) - apply(erule disjoint_subset) - apply(erule disjoint_subset[rotated]) - apply(simp add: ptr_range_def blah word_and_le2) - apply(erule disjoint_subset) - apply(erule disjoint_subset[rotated]) - apply(simp add: ptr_range_def blah word_and_le2) +lemma irq_state_independent_A_only_timer_irq_inv[simp]: + "irq_state_independent_A (only_timer_irq_inv irq st)" + apply (simp add: only_timer_irq_inv_def) + apply (rule irq_state_independent_A_conjI) + apply (simp add: domain_sep_inv_def) + apply (simp add: irq_state_independent_A_def only_timer_irq_def + irq_is_recurring_def is_irq_at_def) done - -lemma invoke_untyped_reads_respects_g: +lemma only_timer_irq_inv_work_units_completed[simp]: + "only_timer_irq_inv irq st (work_units_completed_update f s) + = only_timer_irq_inv irq st s" + apply (simp add: only_timer_irq_inv_def) + apply (simp add: domain_sep_inv_def) + apply (simp add: irq_state_independent_A_def only_timer_irq_def + irq_is_recurring_def is_irq_at_def) + done + +lemma no_irq_freeMemory: + "no_irq (freeMemory ptr sz)" + apply (simp add: freeMemory_def) + apply (wp no_irq_mapM_x no_irq_storeWord) + done + +crunch irq_masks[wp]: delete_objects "\s. P (irq_masks (machine_state s))" + (ignore: do_machine_op wp: dmo_wp no_irq_freeMemory no_irq + simp: detype_def) + +lemma delete_objects_pspace_no_overlap_again: + "\ pspace_aligned and valid_objs and + (\ s. \slot. cte_wp_at (\cp. is_untyped_cap cp \ obj_ref_of cp = ptr \ bits_of cp = sz) slot s) + and K (S \ {ptr .. ptr + 2 ^ sz - 1})\ + delete_objects ptr sz + \\rv. pspace_no_overlap S\" + unfolding delete_objects_def do_machine_op_def + apply(wp | simp add: split_def detype_msu_comm)+ + apply(clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def) + apply(drule caps_of_state_cteD) + apply(frule cte_wp_at_valid_objs_valid_cap, clarsimp+) + apply(erule pspace_no_overlap_subset[rotated]) + apply(rule pspace_no_overlap_subset, rule pspace_no_overlap_detype, simp+) + apply(simp add: valid_cap_simps cap_aligned_def is_aligned_neg_mask_eq field_simps) + done + +lemma reset_untyped_cap_reads_respects_g: + "reads_equiv_valid_g_inv (affects_equiv aag l) aag + (\s. cte_wp_at is_untyped_cap slot s \ invs s \ ct_active s + \ only_timer_irq_inv irq st s + \ is_subject aag (fst slot) + \ (descendants_of slot (cdt s) = {})) + (reset_untyped_cap slot)" + apply (simp add: reset_untyped_cap_def) + apply (rule equiv_valid_guard_imp) + apply (wp set_cap_reads_respects_g dmo_clearMemory_reads_respects_g + | simp add: unless_def when_def split del: split_if)+ + apply (rule_tac I="invs and cte_wp_at (\cp. is_untyped_cap rv + \ (\idx. cp = free_index_update (\_. idx) rv) + \ free_index_of rv \ 2 ^ (bits_of rv) + \ is_subject aag (fst slot)) slot + and pspace_no_overlap (untyped_range rv) + and only_timer_irq_inv irq st + and (\s. descendants_of slot (cdt s) = {})" in mapME_x_ev) + apply (rule equiv_valid_guard_imp) + apply wp + apply (rule reads_respects_g_from_inv) + apply (rule preemption_point_reads_respects[where irq=irq and st=st]) + apply ((wp preemption_point_inv set_cap_reads_respects_g + set_untyped_cap_invs_simple + only_timer_irq_inv_pres[where Q=\, OF _ set_cap_domain_sep_inv] + dmo_clearMemory_reads_respects_g + | simp)+) + apply (strengthen empty_descendants_range_in) + apply (wp only_timer_irq_inv_pres[where P=\ and Q=\] + no_irq_clearMemory + | simp + | wp_once dmo_wp)+ + apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def) + apply (frule(1) caps_of_state_valid) + apply (clarsimp simp: valid_cap_simps cap_aligned_def + is_aligned_neg_mask_eq field_simps + free_index_of_def invs_valid_global_objs) + apply (simp add: aligned_add_aligned is_aligned_shiftl) + apply (frule untyped_caps_do_not_overlap_arm_globals_frame[OF caps_of_state_cteD], + clarsimp+) + apply (subst disjoint_subset[rotated], assumption) + apply (rule Access.ptr_range_subset, simp_all)[1] + apply (simp add: is_aligned_shiftl) + apply (rule shiftl_less_t2n) + apply (rule word_of_nat_less, simp) + apply (simp add: word_bits_def) + apply (clarsimp simp: reset_chunk_bits_def) + apply (rule hoare_pre) + apply (wp preemption_point_inv' set_untyped_cap_invs_simple + set_cap_cte_wp_at set_cap_no_overlap + only_timer_irq_inv_pres[where Q=\, OF _ set_cap_domain_sep_inv] + | simp)+ + apply (strengthen empty_descendants_range_in) + apply (wp only_timer_irq_inv_pres[where P=\ and Q=\] + no_irq_clearMemory + | simp + | wp_once dmo_wp)+ + apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def) + apply (frule(1) caps_of_state_valid) + apply (clarsimp simp: valid_cap_simps cap_aligned_def + is_aligned_neg_mask_eq field_simps + free_index_of_def) + apply (wp delete_objects_reads_respects_g) + apply (strengthen invs_valid_global_objs) + apply (wp add: delete_objects_invs_ex + hoare_vcg_const_imp_lift delete_objects_pspace_no_overlap_again + only_timer_irq_inv_pres[where P=\ and Q=\] + del: Untyped_AI.delete_objects_pspace_no_overlap + | simp)+ + apply (rule get_cap_reads_respects_g) + apply (wp get_cap_wp) + apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def) + apply (frule(1) caps_of_state_valid) + apply (clarsimp simp: valid_cap_simps cap_aligned_def + is_aligned_neg_mask_eq field_simps + free_index_of_def invs_valid_global_objs) + apply (frule untyped_caps_do_not_overlap_arm_globals_frame[OF caps_of_state_cteD], + clarsimp+) + apply (frule valid_global_refsD2, clarsimp+) + apply (clarsimp simp: ptr_range_def[symmetric] global_refs_def + descendants_range_def2) + apply (frule if_unsafe_then_capD[OF caps_of_state_cteD], clarsimp+) + apply (strengthen empty_descendants_range_in) + apply (drule ex_cte_cap_protects[OF _ _ _ _ order_refl], + erule caps_of_state_cteD) + apply (clarsimp simp: descendants_range_def2 empty_descendants_range_in) + apply clarsimp+ + apply (cases slot, fastforce) + done + +lemma equiv_valid_obtain: + assumes fn_eq: "\s t. I s t \ A s t \ P s \ P t \ fn s = fn t" + assumes pr: "\x. equiv_valid I A B (P and (\s. fn s = x)) f" + shows "equiv_valid I A B P f" + apply (clarsimp simp: equiv_valid_def2 equiv_valid_2_def) + apply (frule(1) fn_eq, simp+) + apply (cut_tac x="fn s" in pr) + apply (clarsimp simp: equiv_valid_def2 equiv_valid_2_def) + apply fastforce + done + +lemma reads_equiv_cte_wp_at: + "reads_equiv aag s s' + \ is_subject aag (fst slot) + \ cte_wp_at P slot s = cte_wp_at P slot s'" + apply (frule(1) is_subject_kheap_eq) + apply (simp add: cte_wp_at_cases) + done + +lemma reads_equiv_caps_of_state: + "reads_equiv aag s s' + \ is_subject aag (fst slot) + \ caps_of_state s slot = caps_of_state s' slot" + apply (frule(1) reads_equiv_cte_wp_at[where P="op = (the (caps_of_state s slot))"]) + apply (frule(1) reads_equiv_cte_wp_at[where P="\"]) + apply (auto simp: cte_wp_at_caps_of_state) + done + +lemma untyped_cap_refs_in_kernel_window_helper: + "\ caps_of_state s p = Some (UntypedCap dev ptr sz idx); + cap_refs_in_kernel_window s; + S' \ {ptr .. ptr + 2 ^ sz - 1} \ + \ \r \ S'. arm_kernel_vspace (arch_state s) r = ArmVSpaceKernelWindow" + apply (drule(1) cap_refs_in_kernel_windowD) + apply (simp add: untyped_range_def) + apply blast + done + +lemma invoke_untyped_reads_respects_g_wcap: notes blah[simp del] = untyped_range.simps usable_untyped_range.simps atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex shows - "reads_respects_g aag l (invs and valid_untyped_inv ui and ct_active and authorised_untyped_inv_state aag ui and K (authorised_untyped_inv aag ui)) (invoke_untyped ui)" + "reads_respects_g aag l (invs and valid_untyped_inv_wcap ui (Some (UntypedCap dev ptr sz idx)) + and only_timer_irq_inv irq st + and ct_active and pas_refined aag + and K (authorised_untyped_inv aag ui)) (invoke_untyped ui)" apply(case_tac ui) - apply(rename_tac cslot_ptr word1 word2 apiobject_type nat list dev) - apply(simp add: mapM_x_def[symmetric]) + apply(rename_tac cslot_ptr reset ptr_base ptr' apiobject_type nat list dev') + apply(case_tac "\ (dev' = dev \ ptr = ptr' && ~~ mask sz)") + (* contradictory *) + apply (rule equiv_valid_guard_imp, rule_tac gen_asm_ev'[where P="\" and Q=False], + simp) + apply (clarsimp simp: cte_wp_at_caps_of_state) + apply(simp add: invoke_untyped_def mapM_x_def[symmetric]) apply(wp mapM_x_ev'' create_cap_reads_respects_g hoare_vcg_ball_lift create_cap_valid_global_objs init_arch_objects_reads_respects_g | simp)+ apply(rule_tac Q="\_. invs" in hoare_strengthen_post) apply(wp init_arch_objects_invs_from_restricted) apply(fastforce simp: invs_def) - apply(wp retype_region_reads_respects_g[where slot="slot_of_untyped_inv ui"]) + apply(wp retype_region_reads_respects_g[where sz=sz and slot="slot_of_untyped_inv ui"]) apply(rule_tac Q="\rvc s. - word_object_range_cover_globals apiobject_type word2 sz (length list) s \ (\x\set rvc. is_subject aag x) \ (\x\set rvc. is_aligned x (obj_bits_api apiobject_type nat)) \ ((0::word32) < of_nat (length list)) \ @@ -1143,12 +1204,11 @@ lemma invoke_untyped_reads_respects_g: global_refs s \ set rvc = {} \ (\x\set list. is_subject aag (fst x))" for sz in hoare_strengthen_post) - apply(wp word_object_range_cover_globals_inv - retype_region_ret_is_subject[simplified] - retype_region_global_refs_disjoint - retype_region_ret_pd_aligned - retype_region_aligned_for_init - retype_region_post_retype_invs_spec) + apply(wp retype_region_ret_is_subject[where sz=sz, simplified] + retype_region_global_refs_disjoint[where sz=sz] + retype_region_ret_pd_aligned[where sz=sz] + retype_region_aligned_for_init[where sz=sz] + retype_region_post_retype_invs[where sz=sz]) apply(fastforce simp: global_refs_def intro: post_retype_invs_pspace_alignedI post_retype_invs_valid_arch_stateI @@ -1157,183 +1217,107 @@ lemma invoke_untyped_reads_respects_g: elim: in_set_zipE) apply(rule set_cap_reads_respects_g) apply simp - (* sanitise postcondition *) - apply(rule_tac Q="\rvb s. - (\idx. cte_wp_at - (\c. c = - UntypedCap dev - (word2 && - ~~ mask - (bits_of rv)) - (bits_of rv) - idx) - cslot_ptr s \ - (idx - \ unat - (word2 && - mask - (bits_of rv)) \ - pspace_no_overlap word2 (bits_of rv) s)) \ - invs s \ - range_cover word2 (bits_of rv) - (obj_bits_api apiobject_type nat) (length list) \ - list \ [] \ - word_object_range_cover_globals apiobject_type word2 - (bits_of rv) - (length list) s \ -(\x\{word2..(word2 && - ~~ mask - (bits_of rv)) + - (2 ^ - (bits_of rv) - - 1)}. - is_subject aag x) \ (0::word32) < of_nat (length list) \ -pspace_no_overlap word2 - (bits_of rv) s \ -caps_no_overlap word2 - (bits_of rv) s \ - caps_overlap_reserved - {word2..word2 + - of_nat (length list) * - 2 ^ obj_bits_api apiobject_type nat - - 1} - s \ -region_in_kernel_window - {word2..(word2 && - ~~ mask - (bits_of rv)) + - 2 ^ - (bits_of rv) - - 1} - s \ (apiobject_type = CapTableObject \ 0 < nat) \ -{word2..(word2 && - ~~ mask - (bits_of rv)) + - 2 ^ - bits_of rv - - 1} \ - global_refs s = - {} \ (\x\set list. is_subject aag (fst x)) -" in hoare_strengthen_post) - apply(wp hoare_vcg_ex_lift set_cap_cte_wp_at_cases - hoare_vcg_disj_lift set_cap_no_overlap set_free_index_invs' - word_object_range_cover_globals_inv + apply(wp hoare_vcg_ex_lift set_cap_cte_wp_at_cases + hoare_vcg_disj_lift set_cap_no_overlap + set_free_index_invs_UntypedCap set_untyped_cap_caps_overlap_reserved set_cap_caps_no_overlap region_in_kernel_window_preserved) - apply clarsimp - apply(intro conjI,(fastforce simp: cte_wp_at_caps_of_state)+)[1] apply(wp when_ev delete_objects_reads_respects_g hoare_vcg_disj_lift delete_objects_pspace_no_overlap delete_objects_descendants_range_in - word_object_range_cover_globals_inv delete_objects_caps_no_overlap region_in_kernel_window_preserved get_cap_reads_respects_g get_cap_wp + reset_untyped_cap_reads_respects_g[where irq=irq and st=st] |strengthen invs_valid_global_objs_strg |simp split del: split_if)+ - apply(clarsimp simp: conj_comms cong: conj_cong split del: split_if simp: authorised_untyped_inv_def authorised_untyped_inv_state_def) - apply(drule (1) cte_wp_at_eqD2, clarsimp split del: split_if simp: cte_wp_at_sym) - apply(frule cte_wp_at_valid_objs_valid_cap, simp add: invs_valid_objs) - apply(clarsimp simp: valid_cap_def cap_aligned_def is_aligned_neg_mask_eq bits_of_UntypedCap split del: split_if cong: if_cong) - apply(intro conjI) - apply(clarsimp) - apply(rule conjI) - apply (fastforce dest: untyped_caps_do_not_overlap_global_refs simp: global_refs_def) - apply (rule conjI) - apply(fastforce dest: untyped_caps_do_not_overlap_global_refs simp: global_refs_def) - apply(erule untyped_caps_do_not_overlap_arm_globals_frame, auto simp: invs_def valid_state_def)[1] - apply clarsimp - apply(intro impI conjI) - apply(simp_all add: invs_psp_aligned invs_valid_objs cte_wp_cte_at bits_of_UntypedCap) - apply(clarsimp simp: descendants_range_def2 blah) - apply(rule ssubst[OF free_index_of_UntypedCap]) - apply fastforce - apply(fastforce dest!: untyped_slots_not_in_untyped_range[OF _ _ _ _ _ subset_refl] simp: blah) - apply(fastforce intro!: disjI2) - apply(clarsimp simp: descendants_range_def2 blah) - apply(rule ssubst[OF free_index_of_UntypedCap]) - apply fastforce - apply(fastforce dest!: untyped_slots_not_in_untyped_range[OF _ _ _ _ _ subset_refl] simp: blah) - apply(fastforce intro!: disjI2) - apply(frule range_cover.range_cover_compare_bound) - apply(frule range_cover.unat_of_nat_n) - apply(simp add: shiftl_t2n) - apply(subst unat_mult_power_lem) - apply(erule range_cover.string) - apply(simp add: mult.commute) - apply(fastforce intro!: word_object_range_cover_globalsI) - apply(fastforce simp: ptr_range_def bits_of_UntypedCap p_assoc_help) - apply fastforce - apply(fastforce simp: cte_wp_at_def blah) - apply(fastforce dest!: untyped_slots_not_in_untyped_range[OF _ _ _ _ _ subset_refl] simp: blah) - apply fastforce - apply(clarsimp simp: descendants_range_def2 blah) - apply(rule ssubst[OF free_index_of_UntypedCap]) - apply fastforce - apply(fastforce dest: range_cover_subset') - apply(subgoal_tac "usable_untyped_range - (UntypedCap dev (word2 && ~~ mask sz) sz - (unat - ((word2 && mask sz) + of_nat (length list) * 2 ^ obj_bits_api apiobject_type nat))) \ - {word2..word2 + - of_nat (length list) * 2 ^ obj_bits_api apiobject_type nat - 1} = {}") - apply(subgoal_tac "word2 && mask sz = 0", clarsimp simp: shiftl_t2n mult.commute) - apply(erule subst, rule mask_neg_mask_is_zero) - apply(rule usable_range_disjoint, simp+) - apply(fastforce elim: ex_cte_cap_wp_to_weakenE) - apply assumption - apply fastforce - apply(erule ssubst[OF free_index_of_UntypedCap]) - apply(drule cap_refs_in_kernel_windowD2) - apply(simp add: invs_cap_refs_in_kernel_window) - apply(fastforce simp: cap_range_def blah) - apply(fastforce dest!: untyped_caps_do_not_overlap_global_refs simp: invs_valid_global_refs ptr_range_def) - apply(simp add: invs_valid_global_objs) - apply(rule disjI2) - apply(fastforce intro!: cte_wp_at_pspace_no_overlapI simp: cte_wp_at_sym) - apply(rule disjI1) - apply(simp add: free_index_of_UntypedCap) - apply(simp add: mask_out_sub_mask add.commute mult.commute shiftl_t2n) - apply(erule order_trans) - apply(simp add: range_cover_unat) - apply(simp add: mask_out_sub_mask add.commute mult.commute) - apply (rule le_trans[OF unat_plus_gt]) - apply(subst range_cover.unat_of_nat_n_shift, simp+) - apply(simp add: range_cover.range_cover_compare_bound[simplified add.commute]) - apply(simp add: bits_of_UntypedCap)+ - apply(fastforce intro!: word_object_range_cover_globalsI) - apply(drule_tac x="UntypedCap dev (word2 && ~~ mask sz) sz idx" in spec) - apply(clarsimp simp: ptr_range_def p_assoc_help bits_of_UntypedCap) - apply(erule_tac A="{word2 && ~~ mask sz..b}" for b in bspec) - apply(erule subsetD[rotated]) - apply(simp add: blah word_and_le2) - apply(fastforce intro!: cte_wp_at_pspace_no_overlapI simp: cte_wp_at_sym) - apply(fastforce simp: cte_wp_at_def blah) - apply(fastforce intro!: cte_wp_at_caps_no_overlapI simp: cte_wp_at_sym) - apply(drule range_cover_subset', simp) - apply(erule subset_trans) - apply(simp add: blah word_and_le2) - apply(simp add: shiftl_t2n mask_out_sub_mask add.commute mult.commute) - apply(simp add: mask_out_sub_mask[symmetric]) - apply(rule usable_range_disjoint, simp+) - apply(fastforce elim: ex_cte_cap_wp_to_weakenE) - apply assumption - apply(rule descendants_range_in_subseteq[OF cte_wp_at_caps_descendants_range_inI]) - apply (simp add: cte_wp_at_sym)+ - apply(fastforce dest: range_cover_subset') - apply(simp add: free_index_of_UntypedCap) - apply(drule cap_refs_in_kernel_windowD2) - apply(simp add: invs_cap_refs_in_kernel_window) - apply(clarsimp simp: cap_range_def) - apply(erule region_in_kernel_window_subseteq) - apply(simp add: word_and_le2 blah) - apply(drule untyped_caps_do_not_overlap_global_refs) - apply(simp add: invs_valid_global_refs) - apply(erule disjoint_subset[rotated]) - apply(simp add: ptr_range_def blah word_and_le2) + apply (clarsimp simp only: ) + apply (rule_tac P="authorised_untyped_inv aag ui + \ (\p \ ptr_range ptr sz. is_subject aag p)" in hoare_gen_asmE) + apply (rule validE_validE_R, rule_tac E="\\" and Q="\_. invs and valid_untyped_inv_wcap ui + (Some (UntypedCap dev ptr sz (if reset then 0 else idx))) and ct_active + and (\s. reset \ pspace_no_overlap {ptr .. ptr + 2 ^ sz - 1} s)" + in hoare_post_impErr) + apply (rule hoare_pre, wp hoare_whenE_wp) + apply (rule validE_validE_R, rule hoare_post_impErr, rule reset_untyped_cap_invs_etc) + apply (clarsimp simp only: if_True simp_thms, intro conjI, assumption+) + apply simp + apply (auto simp del: valid_untyped_inv_wcap.simps)[1] + apply (clarsimp simp only: ) + apply (frule(2) invoke_untyped_proofs.intro) + apply (clarsimp simp: cte_wp_at_caps_of_state bits_of_def + free_index_of_def untyped_range_def + split_if[where P="\x. x \ unat v" for v] + split del: split_if) + apply (frule(1) valid_global_refsD2[OF _ invs_valid_global_refs]) + apply (strengthen refl) + apply (clarsimp simp: authorised_untyped_inv_def conj_comms + invoke_untyped_proofs.simps) + apply (simp add: arg_cong[OF mask_out_sub_mask, where f="\y. x - y" for x] + field_simps invoke_untyped_proofs.idx_le_new_offs + invoke_untyped_proofs.idx_compare' + untyped_range_def) + apply (strengthen caps_region_kernel_window_imp[mk_strg I E]) + apply (simp add: invoke_untyped_proofs.simps untyped_range_def + invs_cap_refs_in_kernel_window + atLeastatMost_subset_iff[where b=x and d=x for x] + cong: conj_cong split del: split_if) + apply (intro conjI) + (* mostly clagged from Untyped_AI *) + apply (simp add: atLeastatMost_subset_iff word_and_le2) + + apply (case_tac reset) + apply (clarsimp elim!: pspace_no_overlap_subset del: subsetI + simp: blah word_and_le2) + apply (drule invoke_untyped_proofs.ps_no_overlap) + apply (simp add: field_simps) + + apply (simp add: Int_commute, erule disjoint_subset2[rotated]) + apply (simp add: atLeastatMost_subset_iff word_and_le2) + + apply (clarsimp dest!: invoke_untyped_proofs.idx_le_new_offs) + + apply (simp add: ptr_range_def) + apply (erule ball_subset, rule range_subsetI[OF _ order_refl]) + apply (simp add: word_and_le2) + + apply (erule order_trans[OF invoke_untyped_proofs.subset_stuff]) + apply (simp add: atLeastatMost_subset_iff word_and_le2) + + apply (drule invoke_untyped_proofs.usable_range_disjoint) + apply (clarsimp simp: field_simps mask_out_sub_mask shiftl_t2n) + + apply blast + + apply simp + + apply (clarsimp simp: cte_wp_at_caps_of_state authorised_untyped_inv_def) + apply (strengthen refl) + apply (frule(1) cap_auth_caps_of_state) + apply (simp add: aag_cap_auth_def untyped_range_def + aag_has_Control_iff_owns ptr_range_def[symmetric]) + apply (erule disjE, simp_all)[1] + done + +lemma invoke_untyped_reads_respects_g: + "reads_respects_g aag l (invs and valid_untyped_inv ui + and only_timer_irq_inv irq st + and ct_active and pas_refined aag + and K (authorised_untyped_inv aag ui)) (invoke_untyped ui)" + apply (rule_tac fn="\s. caps_of_state s (slot_of_untyped_inv ui)" in equiv_valid_obtain) + apply (cases ui, clarsimp simp: valid_untyped_inv_wcap reads_equiv_g_def) + apply (simp add: authorised_untyped_inv_def + reads_equiv_caps_of_state) + apply (case_tac "x \ None \ is_untyped_cap (the x)") + apply (clarsimp simp: is_cap_simps) + apply (rule equiv_valid_guard_imp, rule invoke_untyped_reads_respects_g_wcap) + apply (cases ui, clarsimp simp: cte_wp_at_caps_of_state valid_untyped_inv_wcap) + apply auto[1] + apply (rule equiv_valid_guard_imp, rule gen_asm_ev'[where Q=False]) + apply simp + apply (cases ui, clarsimp simp: valid_untyped_inv_wcap cte_wp_at_caps_of_state) done - declare modify_wp [wp del] @@ -1350,201 +1334,83 @@ lemma delete_objects_globals_equiv[wp]: apply (clarsimp simp: ptr_range_def)+ done -fun slots_of_untyped_inv where "slots_of_untyped_inv (Retype _ _ _ _ _ slots _) = slots" +lemma reset_untyped_cap_globals_equiv: + "\globals_equiv st and invs and cte_wp_at is_untyped_cap slot + and ct_active and (\s. descendants_of slot (cdt s) = {})\ + reset_untyped_cap slot + \\_. globals_equiv st\" + apply (simp add: reset_untyped_cap_def) + apply (rule hoare_pre) + apply (wp set_cap_globals_equiv dmo_clearMemory_globals_equiv + preemption_point_inv | simp add: unless_def)+ + apply (rule valid_validE) + apply (rule_tac P="cap_aligned cap \ is_untyped_cap cap" in hoare_gen_asm) + apply (rule_tac Q="\_ s. valid_global_objs s \ globals_equiv st s + \ untyped_range cap \ range_of_arm_globals_frame s = {}" + in hoare_strengthen_post) + apply (rule validE_valid, rule mapME_x_wp') + apply (rule hoare_pre) + apply (wp set_cap_globals_equiv dmo_clearMemory_globals_equiv + preemption_point_inv | simp)+ + apply (clarsimp simp: is_cap_simps ptr_range_def[symmetric] + cap_aligned_def bits_of_def + free_index_of_def) + apply (simp add: aligned_add_aligned is_aligned_shiftl) + apply (subst disjoint_subset[rotated], assumption) + apply (rule Access.ptr_range_subset, simp_all)[1] + apply (simp add: is_aligned_shiftl) + apply (rule shiftl_less_t2n) + apply (rule word_of_nat_less, simp) + apply (simp add: word_bits_def) + apply (clarsimp simp: reset_chunk_bits_def) + apply simp + apply (simp add: if_apply_def2) + apply (strengthen invs_valid_global_objs) + apply (wp delete_objects_invs_ex + hoare_vcg_const_imp_lift get_cap_wp) + apply (clarsimp simp: cte_wp_at_caps_of_state + descendants_range_def2 + is_cap_simps bits_of_def + split del: split_if) + apply (frule caps_of_state_valid_cap, clarsimp+) + apply (frule untyped_caps_do_not_overlap_arm_globals_frame + [OF caps_of_state_cteD], clarsimp+) + apply (clarsimp simp: valid_cap_simps cap_aligned_def) + apply (frule valid_global_refsD2, clarsimp+) + apply (clarsimp simp: ptr_range_def[symmetric] global_refs_def) + apply (strengthen empty_descendants_range_in) + apply (cases slot) + apply fastforce + done lemma invoke_untyped_globals_equiv: notes blah[simp del] = untyped_range.simps usable_untyped_range.simps atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex shows - "\ globals_equiv st and invs and valid_untyped_inv ui and ct_active and - K ((0::word32) < of_nat (length (slots_of_untyped_inv ui))) \ + "\ globals_equiv st and invs and valid_untyped_inv ui and ct_active\ invoke_untyped ui \ \_. globals_equiv st \" - apply(rule hoare_gen_asm) - apply(case_tac ui) - apply(rename_tac cslot_ptr word1 word2 apiobject_type nat list dev) - apply(simp add: mapM_x_def[symmetric]) - apply(wp) - apply(rule_tac Q="\_. globals_equiv st and valid_global_objs" in hoare_strengthen_post) - apply(wp mapM_x_wp[OF _ subset_refl] create_cap_globals_equiv | simp)+ - apply(rule_tac Q="\_. globals_equiv st and invs" in hoare_strengthen_post) - apply(wp init_arch_objects_globals_equiv init_arch_objects_invs_from_restricted) - apply(fastforce simp: invs_def) - apply(rule_tac Q="\ rva s. globals_equiv st s \ word_object_range_cover_globals apiobject_type word2 sz - (length list) s \ - ((0::word32) < of_nat (length list)) \ - (\x\set rva. is_aligned x (obj_bits_api apiobject_type nat)) \ - (post_retype_invs apiobject_type rva s) \ - (global_refs s \ set rva = {})" for sz in hoare_strengthen_post) - apply(wp retype_region_ret_is_subject[simplified] retype_region_global_refs_disjoint - retype_region_ret_pd_aligned retype_region_aligned_for_init retype_region_post_retype_invs_spec - retype_region_globals_equiv[where slot="slot_of_untyped_inv ui"] word_object_range_cover_globals_inv)[1] - apply(auto simp: global_refs_def simp: obj_bits_api_def default_arch_object_def pd_bits_def pageBits_def post_retype_invs_def)[1] - apply (fold ptr_range_def, simp) - apply(rule_tac - Q="\ya s. globals_equiv st s \ - (\idx. cte_wp_at - (\c. c = - UntypedCap dev - (word2 && - ~~ mask - (bits_of cap)) - (bits_of cap) - idx) - cslot_ptr s \ - (idx - \ unat - (word2 && - mask - (bits_of cap)) \ - pspace_no_overlap word2 - (bits_of cap) - s)) \ - invs s \ range_cover word2 - (bits_of cap) - (obj_bits_api apiobject_type nat) (length list) \ - list \ [] \ - word_object_range_cover_globals apiobject_type word2 - (bits_of cap) - (length list) s \ - (0::word32) < of_nat (length list) \ - caps_no_overlap word2 (bits_of cap) s \ - pspace_no_overlap word2 (bits_of cap) s \ - caps_overlap_reserved - {word2..word2 + - of_nat (length list) * - 2 ^ obj_bits_api apiobject_type nat - - 1} - s \ - region_in_kernel_window - {word2..(word2 && - ~~ mask - (bits_of cap)) + - 2 ^ - (bits_of cap) - - 1} - s \ - (apiobject_type = CapTableObject \ 0 < nat) \ -{word2..(word2 && - ~~ mask - (bits_of cap)) + - 2 ^ - (bits_of cap) - - 1} \ - global_refs s = - {} - " in hoare_strengthen_post) - apply (wp set_cap_globals_equiv hoare_vcg_ex_lift set_cap_cte_wp_at_cases - hoare_vcg_disj_lift set_cap_no_overlap set_free_index_invs' - word_object_range_cover_globals_inv set_cap_caps_no_overlap - set_untyped_cap_caps_overlap_reserved - region_in_kernel_window_preserved) - apply clarsimp - apply(intro conjI,(fastforce simp:cte_wp_at_caps_of_state)+)[1] - apply(wp hoare_vcg_ex_lift hoare_vcg_disj_lift - delete_objects_pspace_no_overlap delete_objects_descendants_range_in - word_object_range_cover_globals_inv delete_objects_caps_no_overlap - region_in_kernel_window_preserved get_cap_wp - | simp split del: split_if - | strengthen invs_valid_global_objs_strg)+ - apply(clarsimp simp: conj_comms cong: conj_cong split del: split_if simp: authorised_untyped_inv_def authorised_untyped_inv_state_def) - apply(drule (1) cte_wp_at_eqD2, clarsimp split del: split_if simp: cte_wp_at_sym) - apply(frule cte_wp_at_valid_objs_valid_cap, simp add: invs_valid_objs) - apply(split split_if) - apply(intro impI conjI) - apply(simp_all add: invs_psp_aligned invs_valid_objs cte_wp_cte_at bits_of_UntypedCap) - apply(clarsimp simp: valid_cap_def cap_aligned_def) - apply(rule conjI) - apply (erule untyped_caps_do_not_overlap_arm_globals_frame, (simp add: invs_valid_objs invs_arch_state invs_valid_global_refs)+) - apply(fastforce dest!: untyped_caps_do_not_overlap_global_refs simp: invs_valid_global_refs ptr_range_def global_refs_def) - apply(clarsimp simp: descendants_range_def2 blah) - apply(rule ssubst[OF free_index_of_UntypedCap]) - apply(fastforce simp: ptr_range_def) - apply(fastforce dest!: untyped_slots_not_in_untyped_range[OF _ _ _ _ _ subset_refl] simp: blah ptr_range_def) - apply(fastforce intro!: disjI2) - apply(clarsimp simp: descendants_range_def2 blah) - apply(rule ssubst[OF free_index_of_UntypedCap]) - apply(fastforce simp: ptr_range_def) - apply(fastforce dest!: untyped_slots_not_in_untyped_range[OF _ _ _ _ _ subset_refl] simp: blah ptr_range_def) - apply(fastforce intro!: disjI2 simp: ptr_range_def) - apply(frule range_cover.range_cover_compare_bound) - apply(frule range_cover.unat_of_nat_n) - apply(simp add: shiftl_t2n) - apply(subst unat_mult_power_lem) - apply(erule range_cover.string) - apply(simp add: mult.commute) - apply(fastforce intro!: word_object_range_cover_globalsI) - apply(fastforce simp: ptr_range_def bits_of_UntypedCap p_assoc_help) - apply(fastforce simp: bits_of_UntypedCap) - apply simp - apply(fastforce intro!: word_object_range_cover_globalsI) - apply(fastforce simp: cte_wp_at_def blah) - apply(fastforce dest!: untyped_slots_not_in_untyped_range[OF _ _ _ _ _ subset_refl] simp: blah ptr_range_def) - apply (fastforce simp: ptr_range_def) - apply fastforce - apply(clarsimp simp: descendants_range_def2 blah) - apply(rule ssubst[OF free_index_of_UntypedCap]) - apply(fastforce simp: ptr_range_def) - apply(fastforce dest: range_cover_subset') - apply(subgoal_tac "usable_untyped_range - (UntypedCap dev (word2 && ~~ mask sz) sz - (unat - ((word2 && mask sz) + of_nat (length list) * 2 ^ obj_bits_api apiobject_type nat))) \ - {word2..word2 + - of_nat (length list) * 2 ^ obj_bits_api apiobject_type nat - - 1} = - {}") - apply(subgoal_tac "word2 && mask sz = 0", clarsimp simp: shiftl_t2n mult.commute) - apply(erule subst, rule mask_neg_mask_is_zero) - apply(rule usable_range_disjoint, simp+) - apply(fastforce elim: ex_cte_cap_wp_to_weakenE) - apply assumption - apply(fastforce simp: ptr_range_def) - apply(erule ssubst[OF free_index_of_UntypedCap]) - apply(drule cap_refs_in_kernel_windowD2) - apply(simp add: invs_cap_refs_in_kernel_window) - apply(fastforce simp: cap_range_def blah) - apply(fastforce dest!: untyped_caps_do_not_overlap_global_refs simp: invs_valid_global_refs ptr_range_def) - apply(simp add: invs_valid_global_objs) - apply(rule disjI2) - apply(fastforce intro!: cte_wp_at_pspace_no_overlapI simp: cte_wp_at_sym valid_cap_def cap_aligned_def) - apply(rule conjI, assumption) - apply(rule conjI) - apply(rule disjI1) - apply(simp add: free_index_of_UntypedCap) - apply(simp add: mask_out_sub_mask add.commute mult.commute shiftl_t2n) - apply(erule order_trans) - apply(simp add: range_cover_unat) - apply(simp add: mask_out_sub_mask add.commute mult.commute bits_of_UntypedCap) - apply (rule le_trans[OF unat_plus_gt]) - apply(subst range_cover.unat_of_nat_n_shift, simp+) - apply(simp add: range_cover.range_cover_compare_bound[simplified add.commute]) - apply(fastforce intro!: word_object_range_cover_globalsI) - apply(rule conjI) - apply(fastforce simp: cte_wp_at_def blah) - apply(fastforce intro!: cte_wp_at_caps_no_overlapI simp: cte_wp_at_sym valid_cap_def cap_aligned_def) - apply(fastforce intro!: cte_wp_at_pspace_no_overlapI simp: cte_wp_at_sym valid_cap_def cap_aligned_def) - apply(drule range_cover_subset', simp) - apply(erule subset_trans) - apply(simp add: blah word_and_le2) - apply(simp add: shiftl_t2n mask_out_sub_mask add.commute mult.commute) - apply(simp add: mask_out_sub_mask[symmetric]) - apply(rule usable_range_disjoint, simp+) - apply(fastforce elim: ex_cte_cap_wp_to_weakenE) - apply assumption - apply(rule descendants_range_in_subseteq[OF cte_wp_at_caps_descendants_range_inI]) - apply (simp add: cte_wp_at_sym valid_cap_def cap_aligned_def)+ - apply(fastforce dest: range_cover_subset') - apply(simp add: free_index_of_UntypedCap) - apply(drule cap_refs_in_kernel_windowD2) - apply(simp add: invs_cap_refs_in_kernel_window) - apply(clarsimp simp: cap_range_def) - apply(erule region_in_kernel_window_subseteq) - apply(simp add: word_and_le2 blah) - apply(drule untyped_caps_do_not_overlap_global_refs) - apply(simp add: invs_valid_global_refs) - apply(erule disjoint_subset[rotated]) - apply(simp add: ptr_range_def blah word_and_le2) + apply (rule hoare_name_pre_state) + apply (rule hoare_pre, rule invoke_untyped_Q) + apply (wp create_cap_globals_equiv) + apply auto[1] + apply (wp init_arch_objects_globals_equiv) + apply (clarsimp simp: retype_addrs_aligned_range_cover cte_wp_at_caps_of_state + simp del: valid_untyped_inv_wcap.simps) + apply (frule valid_global_refsD2) + apply (clarsimp simp: post_retype_invs_def split: split_if_asm) + apply (drule disjoint_subset2[rotated]) + apply (rule order_trans, erule retype_addrs_subset_ptr_bits) + apply (simp add: untyped_range_def blah word_and_le2 field_simps) + apply (auto simp: global_refs_def post_retype_invs_def split: split_if_asm)[1] + apply (rule hoare_pre, wp retype_region_globals_equiv[where slot="slot_of_untyped_inv ui"]) + apply (clarsimp simp: cte_wp_at_caps_of_state) + apply (strengthen refl) + apply simp + apply (wp set_cap_globals_equiv) + apply auto[1] + apply (wp reset_untyped_cap_globals_equiv) + apply (cases ui, clarsimp simp: cte_wp_at_caps_of_state) done end diff --git a/proof/infoflow/Syscall_IF.thy b/proof/infoflow/Syscall_IF.thy index 52c05a5d6..46d9061b7 100644 --- a/proof/infoflow/Syscall_IF.thy +++ b/proof/infoflow/Syscall_IF.thy @@ -1107,8 +1107,7 @@ crunch globals_equiv[wp]: invoke_domain "globals_equiv st" lemma perform_invocation_globals_equiv: "\invs and ct_active and valid_invocation oper and globals_equiv (st :: det_ext state) and - authorised_for_globals_inv oper - and K (case oper of (InvokeUntyped i) \ (0::word32) < of_nat (length (slots_of_untyped_inv i)) | _ \ True)\ + authorised_for_globals_inv oper \ perform_invocation blocking calling oper \\_. globals_equiv st\" apply (subst pi_cases) @@ -1128,30 +1127,6 @@ lemma perform_invocation_globals_equiv: authorised_for_globals_inv_def) done -lemma dui_length_slots: - "\\\ - decode_untyped_invocation label args slot cap excaps - \\rv s. (0::word32) < of_nat (length (slots_of_untyped_inv rv))\,-" - unfolding decode_untyped_invocation_def - apply(rule hoare_pre) - apply (simp add: unlessE_def[symmetric] whenE_def[symmetric] unlessE_whenE - split del: split_if) - apply(wp whenE_throwError_wp - |wpc - |simp add: nonzero_unat_simp split del: split_if add: split_def)+ - apply(intro impI, rule TrueI) - done - -lemma di_untyped_length_slots: - "\\\ - decode_invocation label args cap_index slot cap excaps - \\ rv s. (case rv of (InvokeUntyped ui) \ (0::word32) < of_nat (length (slots_of_untyped_inv ui)) | _ \ True)\,-" - unfolding decode_invocation_def - apply(rule hoare_pre) - apply(wp dui_length_slots | wpc | simp add: comp_def split_def uncurry_def)+ - apply auto - done - lemma handle_invocation_globals_equiv: "\invs and ct_active and globals_equiv st\ handle_invocation calling blocking \\_. globals_equiv (st::det_ext state)\" apply (simp add: handle_invocation_def ts_Restart_case_helper split_def @@ -1167,7 +1142,6 @@ lemma handle_invocation_globals_equiv: set_thread_state_ct_st' set_thread_state_globals_equiv sts_authorised_for_globals_inv decode_invocation_authorised_globals_inv - di_untyped_length_slots | simp add: crunch_simps invs_imps)+ apply (auto intro: st_tcb_ex_cap simp: ct_active_not_idle ct_in_state_def) done diff --git a/proof/invariant-abstract/ARM/ArchArch_AI.thy b/proof/invariant-abstract/ARM/ArchArch_AI.thy index adc590b0f..a5d40bdbb 100644 --- a/proof/invariant-abstract/ARM/ArchArch_AI.thy +++ b/proof/invariant-abstract/ARM/ArchArch_AI.thy @@ -706,7 +706,8 @@ lemma perform_asid_control_invocation_st_tcb_at: done lemma set_cap_idx_up_aligned_area: - "\K (pcap = UntypedCap dev ptr pageBits idx) and cte_wp_at (op = pcap) slot and valid_objs\ set_cap (max_free_index_update pcap) slot + "\K (\idx. pcap = UntypedCap dev ptr pageBits idx) and cte_wp_at (op = pcap) slot + and valid_objs\ set_cap (max_free_index_update pcap) slot \\rv s. (\slot. cte_wp_at (\c. up_aligned_area ptr pageBits \ cap_range c \ cap_is_device c = dev) slot s)\" apply (rule hoare_pre) apply (wp hoare_vcg_ex_lift set_cap_cte_wp_at) @@ -717,7 +718,7 @@ lemma set_cap_idx_up_aligned_area: p_assoc_help valid_cap_def valid_untyped_def cap_aligned_def) done -primrec get_untyped_cap_idx :: "cap \ nat" +primrec(nonexhaustive) get_untyped_cap_idx :: "cap \ nat" where "get_untyped_cap_idx (UntypedCap dev ref sz idx) = idx" lemma aci_invs': diff --git a/proof/invariant-abstract/Retype_AI.thy b/proof/invariant-abstract/Retype_AI.thy index c1e07893f..e211996bf 100644 --- a/proof/invariant-abstract/Retype_AI.thy +++ b/proof/invariant-abstract/Retype_AI.thy @@ -290,6 +290,42 @@ lemma aligned_ranges_subset_or_disjoint: apply arith done +lemma aligned_range_offset_subset: + assumes al: "is_aligned (ptr :: 'a :: len word) sz" and al': "is_aligned x sz'" + and szv: "sz' \ sz" and xsz: "x < 2 ^ sz" + shows "{ptr + x .. (ptr + x) + 2 ^ sz' - 1} \ {ptr .. ptr + 2 ^ sz - 1}" + using al +proof (rule is_aligned_get_word_bits) + assume p0: "ptr = 0" and szv': "len_of TYPE ('a) \ sz" + hence "(2 :: 'a word) ^ sz = 0" by simp + + thus ?thesis using p0 + apply - + apply (erule ssubst) + apply simp + done +next + assume szv': "sz < len_of TYPE('a)" + + hence blah: "2 ^ (sz - sz') < (2 :: nat) ^ len_of TYPE('a)" + using szv + apply - + apply (rule power_strict_increasing, simp+) + done + show ?thesis using szv szv' + apply (intro range_subsetI) + apply (rule is_aligned_no_wrap' [OF al xsz]) + apply (simp only: add_diff_eq[symmetric]) + apply (subst add.assoc, rule word_plus_mono_right) + apply (subst iffD1 [OF le_m1_iff_lt]) + apply (simp add: p2_gt_0 word_bits_conv) + apply (rule is_aligned_add_less_t2n[OF al' _ szv xsz]) + apply simp + apply (simp add: field_simps szv al is_aligned_no_overflow) + done +qed + + lemma aligned_diff: "\is_aligned (dest :: 'a :: len word) bits; is_aligned (ptr :: 'a :: len word) sz; bits \ sz; sz < len_of TYPE('a); dest < ptr\