(* * Copyright 2014, General Dynamics C4 Systems * * This software may be distributed and modified according to the terms of * the GNU General Public License version 2. Note that NO WARRANTY is provided. * See "LICENSE_GPLv2.txt" for details. * * @TAG(GD_GPL) *) theory Detype_R imports Retype_R begin context begin interpretation Arch . (*FIXME: arch_split*) text {* Establishing that the invariants are maintained when a region of memory is detyped, that is, removed from the model. *} definition "descendants_range_in' S p \ \m. \p' \ descendants_of' p m. \c n. m p' = Some (CTE c n) \ capRange c \ S = {}" lemma null_filter_simp'[simp]: "null_filter' (null_filter' x) = null_filter' x" apply (rule ext) apply (auto simp:null_filter'_def split:if_splits) done lemma descendants_range_in'_def2: "descendants_range_in' S p = (\m. \p'\descendants_of' p (null_filter' m). \c n. (null_filter' m) p' = Some (CTE c n) \ capRange c \ S = {})" apply (clarsimp simp:descendants_range_in'_def split:if_splits) apply (rule ext) apply (rule subst[OF null_filter_descendants_of']) apply simp apply (rule iffI) apply (clarsimp simp:null_filter'_def)+ apply (drule(1) bspec) apply (elim allE impE ballE) apply (rule ccontr) apply (clarsimp split:if_splits simp:descendants_of'_def) apply (erule(1) subtree_not_Null) apply fastforce apply simp done definition "descendants_range' cap p \ \m. \p' \ descendants_of' p m. \c n. m p' = Some (CTE c n) \ capRange c \ capRange cap = {}" lemma descendants_rangeD': "\ descendants_range' cap p m; m \ p \ p'; m p' = Some (CTE c n) \ \ capRange c \ capRange cap = {}" by (simp add: descendants_range'_def descendants_of'_def) lemma descendants_range_in_lift': assumes st: "\P. \\s. Q s \ P ((swp descendants_of') (null_filter' (ctes_of s)))\ f \\r s. P ((swp descendants_of') (null_filter' (ctes_of s)))\" assumes cap_range: "\P p. \\s. Q' s \ cte_wp_at' (\c. P (capRange (cteCap c))) p s\ f \\r s. cte_wp_at' (\c. P (capRange (cteCap c))) p s\" shows "\\s. Q s \ Q' s \ descendants_range_in' S slot (ctes_of s)\ f \\r s. descendants_range_in' S slot (ctes_of s)\" apply (clarsimp simp:descendants_range_in'_def2) apply (subst swp_def[where f = descendants_of', THEN meta_eq_to_obj_eq, THEN fun_cong, THEN fun_cong, symmetric])+ apply (simp only: Ball_def[unfolded imp_conv_disj]) apply (rule hoare_pre) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift st cap_range) apply (rule_tac Q = "\r s. cte_wp_at' (\c. capRange (cteCap c) \ S = {}) x s" in hoare_strengthen_post) apply (wp cap_range) apply (clarsimp simp:cte_wp_at_ctes_of null_filter'_def) apply clarsimp apply (drule spec, drule(1) mp) apply (subst (asm) null_filter_descendants_of') apply simp apply (case_tac "(ctes_of s) x") apply (clarsimp simp:descendants_of'_def null_filter'_def subtree_target_Some) apply (case_tac a) apply (clarsimp simp:cte_wp_at_ctes_of null_filter'_def split:if_splits) done lemma descendants_range_inD': "\descendants_range_in' S p ms; p'\descendants_of' p ms; ms p' = Some cte\ \ capRange (cteCap cte) \ S = {}" apply (case_tac cte) apply (auto simp:descendants_range_in'_def cte_wp_at_ctes_of dest!:bspec) done end interpretation clear_um: p_arch_idle_update_int_eq "clear_um S" by unfold_locales (simp_all add: clear_um_def) context begin interpretation Arch . (*FIXME: arch_split*) lemma descendants_range'_def2: "descendants_range' cap p = descendants_range_in' (capRange cap) p" by (simp add: descendants_range_in'_def descendants_range'_def) defs deletionIsSafe_def: "deletionIsSafe \ \ptr bits s. \p t m. (cte_wp_at' (\cte. cteCap cte = capability.ReplyCap t m) p s \ t \ {ptr .. ptr + 2 ^ bits - 1}) \ (\ko. ksPSpace s p = Some (KOArch ko) \ p \ {ptr .. ptr + 2 ^ bits - 1} \ 6 \ bits)" defs ksASIDMapSafe_def: "ksASIDMapSafe \ \s. \asid hw_asid pd. armKSASIDMap (ksArchState s) asid = Some (hw_asid,pd) \ page_directory_at' pd s" defs cNodePartialOverlap_def: "cNodePartialOverlap \ \cns inRange. \p n. cns p = Some n \ (\ is_aligned p (cte_level_bits + n) \ cte_level_bits + n \ word_bits \ (\ {p .. p + 2 ^ (cte_level_bits + n) - 1} \ {p. inRange p} \ \ {p .. p + 2 ^ (cte_level_bits + n) - 1} \ {p. \ inRange p}))" (* FIXME: move *) lemma deleteObjects_def2: "is_aligned ptr bits \ deleteObjects ptr bits = do stateAssert (deletionIsSafe ptr bits) []; doMachineOp (freeMemory ptr bits); stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) (\x. x \ {ptr .. ptr + 2 ^ bits - 1})) []; modify (\s. s \ ksPSpace := \x. if x \ {ptr .. ptr + 2 ^ bits - 1} then None else ksPSpace s x, gsUserPages := \x. if x \ {ptr .. ptr + 2 ^ bits - 1} then None else gsUserPages s x, gsCNodes := \x. if x \ {ptr .. ptr + 2 ^ bits - 1} then None else gsCNodes s x \); stateAssert ksASIDMapSafe [] od" apply (simp add: deleteObjects_def is_aligned_mask[symmetric] unless_def) apply (rule bind_eqI, rule ext) apply (rule bind_eqI, rule ext) apply (simp add: bind_assoc[symmetric]) apply (rule bind_cong[rotated], rule refl) apply (simp add: bind_assoc modify_modify deleteRange_def gets_modify_def) apply (rule ext, simp add: exec_modify stateAssert_def assert_def bind_assoc exec_get NOT_eq[symmetric] mask_in_range) apply (clarsimp simp: simpler_modify_def) apply (simp add: data_map_filterWithKey_def split: if_split_asm) apply (rule arg_cong2[where f=gsCNodes_update]) apply (simp add: NOT_eq[symmetric] mask_in_range ext) apply (rule arg_cong2[where f=gsUserPages_update]) apply (simp add: NOT_eq[symmetric] mask_in_range ext) apply (rule arg_cong[where f="\f. ksPSpace_update f s" for s]) apply (simp add: NOT_eq[symmetric] mask_in_range ext split: option.split) done lemma deleteObjects_def3: "deleteObjects ptr bits = do assert (is_aligned ptr bits); stateAssert (deletionIsSafe ptr bits) []; doMachineOp (freeMemory ptr bits); stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) (\x. x \ {ptr .. ptr + 2 ^ bits - 1})) []; modify (\s. s \ ksPSpace := \x. if x \ {ptr .. ptr + 2 ^ bits - 1} then None else ksPSpace s x, gsUserPages := \x. if x \ {ptr .. ptr + 2 ^ bits - 1} then None else gsUserPages s x, gsCNodes := \x. if x \ {ptr .. ptr + 2 ^ bits - 1} then None else gsCNodes s x \); stateAssert ksASIDMapSafe [] od" apply (cases "is_aligned ptr bits") apply (simp add: deleteObjects_def2) apply (simp add: deleteObjects_def is_aligned_mask unless_def alignError_def) done lemma obj_relation_cuts_in_obj_range: "\ (y, P) \ obj_relation_cuts ko x; x \ obj_range x ko; kheap s x = Some ko; valid_objs s; pspace_aligned s \ \ y \ obj_range x ko" apply (cases ko, simp_all) apply (clarsimp split: if_split_asm) apply (subgoal_tac "cte_at (x, ya) s") apply (drule(2) cte_at_cte_map_in_obj_bits) apply (simp add: obj_range_def) apply (fastforce intro: cte_wp_at_cteI) apply (frule(1) pspace_alignedD) apply (frule valid_obj_sizes, erule ranI) apply (rename_tac arch_kernel_obj) apply (case_tac arch_kernel_obj, simp_all) apply (clarsimp simp only: obj_range_def field_simps atLeastAtMost_iff obj_bits.simps arch_kobj_size.simps) apply (rule context_conjI) apply (erule is_aligned_no_wrap') apply simp apply (simp add: ucast_less_shiftl_helper) apply (subst add_diff_eq[symmetric]) apply (rule word_plus_mono_right) apply (subst word_less_sub_le, simp) apply (simp add: ucast_less_shiftl_helper) apply (simp add: field_simps) apply (clarsimp simp only: obj_range_def field_simps atLeastAtMost_iff obj_bits.simps arch_kobj_size.simps) apply (rule context_conjI) apply (erule is_aligned_no_wrap') apply simp apply (simp add: ucast_less_shiftl_helper) apply (subst add_diff_eq[symmetric]) apply (rule word_plus_mono_right) apply (subst word_less_sub_le, simp) apply (simp add: ucast_less_shiftl_helper) apply (simp add: field_simps) apply (rename_tac vmpage_size) apply (clarsimp simp only: obj_range_def field_simps atLeastAtMost_iff obj_bits.simps arch_kobj_size.simps) apply (subgoal_tac "n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size") apply (rule context_conjI) apply (erule is_aligned_no_wrap') apply assumption apply (subst add_diff_eq[symmetric]) apply (rule word_plus_mono_right) apply (subst word_less_sub_le, simp add: word_bits_def) apply assumption apply (simp add: field_simps) apply (erule word_less_power_trans2) apply (case_tac vmpage_size, simp_all add: pageBits_def)[1] apply (simp add: word_bits_def) done lemma obj_relation_cuts_eqv_base_in_detype_range: "\ (y, P) \ obj_relation_cuts ko x; kheap s x = Some ko; valid_objs s; pspace_aligned s; valid_untyped (cap.UntypedCap d base bits idx) s \ \ (x \ {base .. base + 2 ^ bits - 1}) = (y \ {base .. base + 2 ^ bits - 1})" apply (simp add: valid_untyped_def del: atLeastAtMost_iff) apply (subgoal_tac "x \ obj_range x ko") apply (subgoal_tac "y \ obj_range x ko") apply blast apply (erule(4) obj_relation_cuts_in_obj_range) apply (simp add: obj_range_def) apply (rule is_aligned_no_overflow) apply (erule(1) pspace_alignedD) done lemma detype_pspace_relation: assumes psp: "pspace_relation (kheap s) (ksPSpace s')" and bwb: "bits < word_bits" and al: "is_aligned base bits" and vs: "valid_pspace s" and vu: "valid_untyped (cap.UntypedCap d base bits idx) s" shows "pspace_relation (kheap (detype {base .. base + 2 ^ bits - 1} s)) (\x. if x \ {base .. base + 2 ^ bits - 1} then None else ksPSpace s' x)" (is "pspace_relation ?ps ?ps'") proof - let ?range = "{base .. base + 2 ^ bits - 1}" let ?ps'' = "(kheap s |` (-?range))" have pa: "pspace_aligned s" and vo: "valid_objs s" using vs by (simp add: valid_pspace_def)+ have pspace: "\x. \ x \ ?range; x \ dom (kheap s) \ \ ?ps x = kheap s x" by (clarsimp simp add: detype_def field_simps) have pspace'': "\x. \ x \ ?range; x \ dom (kheap s) \ \ ?ps'' x = kheap s x" by (clarsimp simp add: detype_def) have psdom_pre: "dom ?ps = (dom (kheap s) - ?range)" by (fastforce simp:field_simps) show ?thesis unfolding pspace_relation_def proof (intro conjI) have domeq': "dom (ksPSpace s') = pspace_dom (kheap s)" using psp by (simp add: pspace_relation_def) note eqv_base_in = obj_relation_cuts_eqv_base_in_detype_range [OF _ _ vo pa vu] note atLeastAtMost_iff[simp del] show domeq: "pspace_dom ?ps = dom ?ps'" apply (simp add: dom_if_None domeq') apply (simp add: pspace_dom_def detype_def dom_if_None) apply (intro set_eqI iffI, simp_all) apply (clarsimp simp: eqv_base_in field_simps) apply (rule rev_bexI, erule domI) apply (simp add: image_def, erule rev_bexI, simp) apply (elim exE bexE DiffE conjE domE) apply (rule bexI, assumption) apply (clarsimp simp add: eqv_base_in field_simps) done show "\x\dom ?ps. \(y, P)\obj_relation_cuts (the (?ps x)) x. P (the (?ps x)) (the (if y \ ?range then None else ksPSpace s' y))" using psp apply (simp add: pspace_relation_def psdom_pre split del: if_split) apply (erule conjE, rule ballI, erule DiffE, drule(1) bspec) apply (erule domE) apply (simp add: field_simps detype_def cong: conj_cong) apply (erule ballEI, clarsimp) apply (simp add: eqv_base_in) done qed qed declare plus_Collect_helper2[simp] lemma cte_map_obj_range_helper: "\ cte_at cref s; pspace_aligned s; valid_objs s \ \ \ko. kheap s (fst cref) = Some ko \ cte_map cref \ obj_range (fst cref) ko" apply (drule(2) cte_at_cte_map_in_obj_bits) apply (clarsimp simp: obj_range_def) done lemma cte_map_untyped_range: "\ s \ cap; cte_at cref s; pspace_aligned s; valid_objs s \ \ (cte_map cref \ untyped_range cap) = (fst cref \ untyped_range cap)" apply (cases cap, simp_all) apply (drule(2) cte_map_obj_range_helper) apply (clarsimp simp: valid_cap_def valid_untyped_def) apply (elim allE, drule(1) mp) apply (rule iffI) apply (erule impE) apply (rule notemptyI[where x="cte_map cref"]) apply simp apply clarsimp apply (drule subsetD [OF _ p_in_obj_range]) apply simp+ apply (erule impE) apply (rule notemptyI[where x="fst cref"]) apply (simp add: p_in_obj_range) apply clarsimp apply (drule(1) subsetD) apply simp done lemma pspace_aligned'_cut: "pspace_aligned' s \ pspace_aligned' (s \ ksPSpace := \x. if P x then None else ksPSpace s x\)" by (simp add: pspace_aligned'_def dom_if_None) lemma pspace_distinct'_cut: "pspace_distinct' s \ pspace_distinct' (s \ ksPSpace := \x. if P x then None else ksPSpace s x\)" by (simp add: pspace_distinct'_def dom_if_None ps_clear_def Diff_Int_distrib) lemma ko_wp_at_delete': "pspace_distinct' s \ ko_wp_at' P p (s \ ksPSpace := \x. if base \ x \ x \ base + (2 ^ magnitude - 1) then None else ksPSpace s x \) = (\ (base \ p \ p \ base + (2 ^ magnitude - 1)) \ ko_wp_at' P p s)" apply (simp add: ko_wp_at'_def projectKOs ps_clear_def dom_if_None) apply (intro impI iffI) apply clarsimp apply (drule(1) pspace_distinctD') apply (simp add: ps_clear_def) apply (clarsimp simp: Diff_Int_distrib) done lemma obj_at_delete': "pspace_distinct' s \ obj_at' P p (s \ ksPSpace := \x. if base \ x \ x \ base + (2 ^ magnitude - 1) then None else ksPSpace s x \) = (\ (base \ p \ p \ base + (2 ^ magnitude - 1)) \ obj_at' P p s)" unfolding obj_at'_real_def by (rule ko_wp_at_delete') lemma cte_wp_at_delete': "\ s \' UntypedCap d base magnitude idx; pspace_distinct' s \ \ cte_wp_at' P p (s \ ksPSpace := \x. if base \ x \ x \ base + (2 ^ magnitude - 1) then None else ksPSpace s x \) = (\ (base \ p \ p \ base + (2 ^ magnitude - 1)) \ cte_wp_at' P p s)" apply (simp add: cte_wp_at_obj_cases' obj_at_delete') apply (subgoal_tac "\Q n. obj_at' Q (p - n) s \ tcb_cte_cases n \ None \ ((p - n) \ {base .. base + (2 ^ magnitude - 1)}) = (p \ {base .. base + (2 ^ magnitude - 1)})") apply auto[1] apply (clarsimp simp: obj_at'_real_def projectKOs valid_cap'_def valid_untyped'_def simp del: atLeastAtMost_iff) apply (drule_tac x="p - n" in spec) apply (clarsimp simp: ko_wp_at'_def capAligned_def simp del: atLeastAtMost_iff) apply (thin_tac "is_aligned x 4" for x) apply (drule(1) aligned_ranges_subset_or_disjoint) apply (subgoal_tac "{p, p - n} \ obj_range' (p - n) (KOTCB obj)") apply (clarsimp simp del: atLeastAtMost_iff simp: field_simps objBits_simps obj_range'_def) apply fastforce apply (simp add: obj_range'_def mask_in_range[symmetric] del: atLeastAtMost_iff) apply (simp add: objBits_simps) apply (frule(1) tcb_cte_cases_aligned_helpers) apply (simp add: is_aligned_neg_mask_eq) done lemma map_to_ctes_delete: assumes vc: "s \' UntypedCap d base magnitude idx" and vs: "pspace_distinct' s" shows "map_to_ctes (\x. if base \ x \ x \ base + (2 ^ magnitude - 1) then None else ksPSpace s x) = (\x. if base \ x \ x \ base + (2 ^ magnitude - 1) then None else ctes_of s x)" using cte_wp_at_delete' [where P="op = cte" for cte, OF vc vs] arg_cong [where f=Not, OF cte_wp_at_delete' [OF vc vs, where P="\"]] apply (simp (no_asm_use) add: cte_wp_at_ctes_of) apply (rule ext) apply (case_tac "map_to_ctes (\x. if base \ x \ x \ base + (2 ^ magnitude - 1) then None else ksPSpace s x) x") apply (fastforce split: if_split_asm) apply simp done lemma word_range_card: "base \base + h \ card {base..base + (h::word32)} = (unat h) + 1" proof (induct h) case 1 show ?case by simp next case (2 h) have interval_plus_one_word32: "\base ceil. \base \ ceil + 1;ceil \ ceil + 1\ \ {base..ceil + 1} = {base .. ceil } \ {ceil + (1::word32)}" by (auto intro:order_antisym simp:not_le inc_le) show ?case apply (subst add.commute[where a = 1]) apply (subst add.assoc[symmetric]) apply (subst interval_plus_one_word32) using 2 apply (simp add: field_simps) apply (subst add.assoc) apply (rule word_plus_mono_right) using 2 plus_one_helper2[where n = h and x = h,simplified] apply (simp add: field_simps) using 2 apply (simp add: field_simps) apply (subst card_Un_disjoint,simp+) using 2 apply (clarsimp simp: field_simps) using 2 apply (subst 2) apply (erule word_plus_mono_right2) using 2 plus_one_helper2[where n = h and x = h,simplified] apply (simp add: field_simps) apply simp apply (simp add: unatSuc) done qed end locale detype_locale' = detype_locale + constrains s::"det_state" lemma (in detype_locale') deletionIsSafe: assumes sr: "(s, s') \ state_relation" and cap: "cap = cap.UntypedCap d base magnitude idx" and vs: "valid_pspace s" and al: "is_aligned base magnitude" and vu: "valid_untyped (cap.UntypedCap d base magnitude idx) s" shows "deletionIsSafe base magnitude s'" proof - interpret Arch . (* FIXME: arch_split *) note blah[simp del] = atLeastatMost_subset_iff atLeastLessThan_iff Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex atLeastAtMost_iff have "\t m. \ptr. cte_wp_at (op = (cap.ReplyCap t m)) ptr s \ t \ {base .. base + 2 ^ magnitude - 1}" by (fastforce dest!: valid_cap2 simp: cap obj_reply_refs_def) hence "\ptr t m. cte_wp_at (op = (cap.ReplyCap t m)) ptr s \ t \ {base .. base + 2 ^ magnitude - 1}" by (fastforce simp del: split_paired_All) hence "\t. t \ {base .. base + 2 ^ magnitude - 1} \ (\ptr m. \ cte_wp_at (op = (cap.ReplyCap t m)) ptr s)" by fastforce hence cte: "\t. t \ {base .. base + 2 ^ magnitude - 1} \ (\ptr m. \ cte_wp_at' (\cte. cteCap cte = ReplyCap t m) ptr s')" unfolding deletionIsSafe_def apply - apply (erule allEI) apply (rule impI, drule(1) mp) apply (thin_tac "t \ S" for S) apply (intro allI) apply (clarsimp simp: cte_wp_at_neg2 cte_wp_at_ctes_of simp del: split_paired_All) apply (frule pspace_relation_cte_wp_atI [rotated]) apply (rule invs_valid_objs [OF invs]) apply (rule state_relation_pspace_relation [OF sr]) apply (clarsimp simp: cte_wp_at_neg2 simp del: split_paired_All) apply (drule_tac x="(a,b)" in spec) apply (clarsimp simp: cte_wp_cte_at cte_wp_at_caps_of_state) apply (case_tac c, simp_all) apply fastforce done have arch: "\ ko p. \ ksPSpace s' p = Some (KOArch ko); p \ {base..base + 2 ^ magnitude - 1} \ \ 6 \ magnitude" using sr vs vu apply (clarsimp simp: state_relation_def) apply (erule(1) pspace_dom_relatedE) apply (frule obj_relation_cuts_eqv_base_in_detype_range[symmetric]) apply simp apply (clarsimp simp:valid_pspace_def)+ apply simp apply (clarsimp simp:valid_untyped_def) apply (drule spec)+ apply (erule(1) impE) apply (erule impE) apply (drule p_in_obj_range) apply (clarsimp)+ apply blast apply clarsimp apply (drule card_mono[rotated]) apply fastforce apply (clarsimp simp:valid_pspace_def obj_range_def p_assoc_help) apply (subst (asm) word_range_card) apply (rule is_aligned_no_overflow') apply (erule(1) pspace_alignedD) apply (subst (asm) word_range_card) apply (rule is_aligned_no_overflow'[OF al]) apply (rule ccontr) apply (simp add:not_le) apply (subgoal_tac "obj_bits koa < 32") prefer 2 apply (case_tac koa,simp_all add:objBits_simps word_bits_def) apply (drule(1) valid_cs_size_objsI) apply (clarsimp simp:valid_cs_size_def word_bits_def cte_level_bits_def) apply (rename_tac arch_kernel_obj) apply (case_tac arch_kernel_obj,simp_all add:pageBits_def word_bits_def) apply (simp add:pageBitsForSize_def split:vmpage_size.splits) apply (subgoal_tac "6 \ obj_bits koa") apply simp apply (case_tac koa, simp_all add: other_obj_relation_def objBits_simps cte_relation_def split: if_splits) apply (rename_tac arch_kernel_obj, case_tac arch_kernel_obj; simp add: arch_kobj_size_def pageBits_def pageBitsForSize_def)+ done thus ?thesis using cte by (auto simp: deletionIsSafe_def) qed context begin interpretation Arch . (*FIXME: arch_split*) lemma ksASIDMapSafeI: "\ (s,s') \ state_relation; invs s; pspace_aligned' s' \ pspace_distinct' s' \ \ ksASIDMapSafe s'" apply (clarsimp simp: ksASIDMapSafe_def) apply (subgoal_tac "valid_asid_map s") prefer 2 apply fastforce apply (clarsimp simp: valid_asid_map_def graph_of_def) apply (subgoal_tac "arm_asid_map (arch_state s) asid = Some (hw_asid, pd)") prefer 2 apply (clarsimp simp: state_relation_def arch_state_relation_def) apply (erule allE)+ apply (erule (1) impE) apply clarsimp apply (drule find_pd_for_asid_eq_helper) apply fastforce apply assumption apply fastforce apply clarsimp apply (rule pspace_relation_pd) apply (fastforce simp: state_relation_def) apply fastforce apply assumption apply assumption apply simp done (* FIXME: generalizes lemma SubMonadLib.corres_submonad *) (* FIXME: generalizes lemma SubMonad_R.corres_machine_op *) (* FIXME: move *) lemma corres_machine_op: assumes P: "corres_underlying Id False True r P Q x x'" shows "corres r (P \ machine_state) (Q \ ksMachineState) (do_machine_op x) (doMachineOp x')" apply (rule corres_submonad3 [OF submonad_do_machine_op submonad_doMachineOp _ _ _ _ P]) apply (simp_all add: state_relation_def swp_def) done lemma ekheap_relation_detype: "ekheap_relation ekh kh \ ekheap_relation (\x. if P x then None else (ekh x)) (\x. if P x then None else (kh x))" by (fastforce simp add: ekheap_relation_def split: if_split_asm) lemma cap_table_at_gsCNodes_eq: "(s, s') \ state_relation \ (gsCNodes s' ptr = Some bits) = cap_table_at bits ptr s" apply (clarsimp simp: state_relation_def ghost_relation_def obj_at_def is_cap_table) apply (drule_tac x = ptr in spec)+ apply (drule_tac x = bits in spec)+ apply fastforce done lemma cNodeNoPartialOverlap: "corres dc (\s. \cref. cte_wp_at (op = (cap.UntypedCap d base magnitude idx)) cref s \ valid_objs s \ pspace_aligned s) \ (return x) (stateAssert (\s. \ cNodePartialOverlap (gsCNodes s) (\x. base \ x \ x \ base + 2 ^ magnitude - 1)) [])" apply (simp add: stateAssert_def assert_def) apply (rule corres_symb_exec_r[OF _ get_sp]) apply (rule corres_req[rotated], subst if_P, assumption) apply simp apply (clarsimp simp: cNodePartialOverlap_def) apply (drule(1) cte_wp_valid_cap) apply (clarsimp simp: valid_cap_def valid_untyped_def cap_table_at_gsCNodes_eq obj_at_def is_cap_table) apply (frule(1) pspace_alignedD) apply simp apply (elim allE, drule(1) mp, simp add: obj_range_def valid_obj_def cap_aligned_def) apply (erule is_aligned_get_word_bits[where 'a=32, folded word_bits_def]) apply (clarsimp simp: is_aligned_no_overflow) apply (blast intro: order_trans) apply (simp add: is_aligned_no_overflow power_overflow word_bits_def) apply wp done declare wrap_ext_det_ext_ext_def[simp] lemma detype_corres: "is_aligned base magnitude \ magnitude \ 2 \ corres dc (\s. einvs s \ s \ (cap.UntypedCap d base magnitude idx) \ (\cref. cte_wp_at (op = (cap.UntypedCap d base magnitude idx)) cref s \ descendants_range (cap.UntypedCap d base magnitude idx) cref s) \ untyped_children_in_mdb s \ if_unsafe_then_cap s \ valid_mdb s \ valid_global_refs s \ ct_active s) (\s. s \' (UntypedCap d base magnitude idx) \ valid_pspace' s) (delete_objects base magnitude) (deleteObjects base magnitude)" apply (simp add: deleteObjects_def2) apply (rule corres_stateAssert_implied[where P'=\, simplified]) prefer 2 apply clarsimp apply (rule_tac cap="cap.UntypedCap d base magnitude idx" and ptr="(a,b)" and s=s in detype_locale'.deletionIsSafe, simp_all add: detype_locale'_def detype_locale_def p_assoc_help invs_valid_pspace)[1] apply (simp add:valid_cap_simps) apply (simp add: bind_assoc[symmetric]) apply (rule corres_stateAssert_implied2) defer apply (erule ksASIDMapSafeI, assumption, assumption) apply (rule hoare_pre) apply (rule delete_objects_invs) apply fastforce apply (simp add: doMachineOp_def split_def) apply wp apply (clarsimp simp: valid_pspace'_def pspace_distinct'_def pspace_aligned'_def) apply (rule conjI) subgoal by fastforce apply (clarsimp simp add: pspace_distinct'_def ps_clear_def dom_if_None Diff_Int_distrib) apply (simp add: delete_objects_def) apply (rule_tac Q="\_ s. valid_objs s \ valid_list s \ (\cref. cte_wp_at (op = (cap.UntypedCap d base magnitude idx)) cref s \ descendants_range (cap.UntypedCap d base magnitude idx) cref s ) \ s \ cap.UntypedCap d base magnitude idx \ pspace_aligned s \ valid_mdb s \ pspace_distinct s \ if_live_then_nonz_cap s \ zombies_final s \ sym_refs (state_refs_of s) \ untyped_children_in_mdb s \ if_unsafe_then_cap s \ valid_global_refs s" and Q'="\_ s. s \' capability.UntypedCap d base magnitude idx \ valid_pspace' s" in corres_split') apply (rule corres_bind_return) apply (rule corres_guard_imp[where r=dc]) apply (rule corres_split[OF cNodeNoPartialOverlap]) apply (rule corres_machine_op[OF corres_Id], simp+) apply (rule no_fail_freeMemory, simp+) apply (wp hoare_vcg_ex_lift) apply auto[1] apply (auto elim: is_aligned_weaken) apply (rule corres_modify) apply (simp add: valid_pspace'_def) apply (rule state_relation_null_filterE, assumption, simp_all add: pspace_aligned'_cut pspace_distinct'_cut)[1] apply (simp add: detype_def, rule state.equality; simp add: detype_ext_def) apply (intro exI, fastforce) apply (rule ext, clarsimp simp add: null_filter_def) apply (rule sym, rule ccontr, clarsimp) apply (drule(4) cte_map_not_null_outside') apply (fastforce simp add: cte_wp_at_caps_of_state) apply simp apply (rule ext, clarsimp simp add: null_filter'_def map_to_ctes_delete[simplified field_simps]) apply (rule sym, rule ccontr, clarsimp) apply (frule(2) pspace_relation_cte_wp_atI [OF state_relation_pspace_relation]) apply (elim exE) apply (frule(4) cte_map_not_null_outside') apply (rule cte_wp_at_weakenE, erule conjunct1) apply (case_tac y, clarsimp) apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) apply clarsimp apply (frule_tac cref="(aa, ba)" in cte_map_untyped_range, erule cte_wp_at_weakenE[OF _ TrueI], assumption+) apply simp apply (rule detype_pspace_relation[simplified], simp_all add: state_relation_pspace_relation valid_pspace_def)[1] apply (simp add: valid_cap'_def capAligned_def) apply (clarsimp simp: valid_cap_def, assumption) apply (fastforce simp add: detype_def detype_ext_def intro!: ekheap_relation_detype) apply (clarsimp simp: state_relation_def ghost_relation_of_heap detype_def) apply (drule_tac t="gsUserPages s'" in sym) apply (drule_tac t="gsCNodes s'" in sym) apply (auto simp add: ups_of_heap_def cns_of_heap_def ext split: option.splits kernel_object.splits)[1] apply (simp add: valid_mdb_def) apply (wp hoare_vcg_ex_lift hoare_vcg_ball_lift | wps | simp add: invs_def valid_state_def valid_pspace_def descendants_range_def | wp_once hoare_drop_imps)+ done text {* Invariant preservation across concrete deletion *} lemma caps_containedD': "\ ctes_of s p = Some cte; ctes_of s p' = Some cte'; \ isUntypedCap (cteCap cte); capRange (cteCap cte) \ untypedRange (cteCap cte') \ {}; caps_contained' (ctes_of s) \ \ capRange (cteCap cte) \ untypedRange (cteCap cte')" apply (cases cte, cases cte') apply (simp add: caps_contained'_def) apply blast done lemma untyped_mdbD': "\ ctes p = Some cte; ctes p' = Some cte'; isUntypedCap (cteCap cte); capRange (cteCap cte') \ untypedRange (cteCap cte) \ {}; \ isUntypedCap (cteCap cte'); untyped_mdb' ctes \ \ p' \ descendants_of' p ctes" by (cases cte, cases cte', simp add: untyped_mdb'_def) lemma ko_wp_at_state_refs_ofD: "\ ko_wp_at' P p s \ \ (\ko. P ko \ state_refs_of' s p = refs_of' ko)" by (fastforce simp: ko_wp_at'_def state_refs_of'_def) lemma sym_refs_ko_wp_atD: "\ ko_wp_at' P p s; sym_refs (state_refs_of' s) \ \ (\ko. P ko \ state_refs_of' s p = refs_of' ko \ (\(x, tp) \ refs_of' ko. (p, symreftype tp) \ state_refs_of' s x))" apply (clarsimp dest!: ko_wp_at_state_refs_ofD) apply (rule exI, erule conjI) apply (drule sym) apply clarsimp apply (erule(1) sym_refsD) done lemma zobj_refs_capRange: "capAligned c \ zobj_refs' c \ capRange c" by (cases c, simp_all add: capRange_def capAligned_def is_aligned_no_overflow) end locale delete_locale = fixes s and base and bits and ptr and idx and d assumes cap: "cte_wp_at' (\cte. cteCap cte = UntypedCap d base bits idx) ptr s" and nodesc: "descendants_range' (UntypedCap d base bits idx) ptr (ctes_of s)" and invs: "invs' s" and ct_act: "ct_active' s" and sa_simp: "sch_act_simple s" and bwb: "bits < word_bits" and al: "is_aligned base bits" and safe: "deletionIsSafe base bits s" context delete_locale begin interpretation Arch . (*FIXME: arch_split*) lemma valid_objs: "valid_objs' s" and pa: "pspace_aligned' s" and pd: "pspace_distinct' s" and vq: "valid_queues s" and vq': "valid_queues' s" and sym_refs: "sym_refs (state_refs_of' s)" and iflive: "if_live_then_nonz_cap' s" and ifunsafe: "if_unsafe_then_cap' s" and dlist: "valid_dlist (ctes_of s)" and no_0: "no_0 (ctes_of s)" and chain_0: "mdb_chain_0 (ctes_of s)" and badges: "valid_badges (ctes_of s)" and contained: "caps_contained' (ctes_of s)" and chunked: "mdb_chunked (ctes_of s)" and umdb: "untyped_mdb' (ctes_of s)" and uinc: "untyped_inc' (ctes_of s)" and nullcaps: "valid_nullcaps (ctes_of s)" and ut_rev: "ut_revocable' (ctes_of s)" and dist_z: "distinct_zombies (ctes_of s)" and irq_ctrl: "irq_control (ctes_of s)" and clinks: "class_links (ctes_of s)" and rep_r_fb: "reply_masters_rvk_fb (ctes_of s)" and idle: "valid_idle' s" and refs: "valid_global_refs' s" and arch: "valid_arch_state' s" and virq: "valid_irq_node' (irq_node' s) s" and virqh: "valid_irq_handlers' s" and virqs: "valid_irq_states' s" and no_0_objs: "no_0_obj' s" and ctnotinQ: "ct_not_inQ s" and pde_maps: "valid_pde_mappings' s" and irqs_masked: "irqs_masked' s" and ctcd: "ct_idle_or_in_cur_domain' s" and cdm: "ksCurDomain s \ maxDomain" and vds: "valid_dom_schedule' s" using invs by (auto simp add: invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def valid_mdb_ctes_def) abbreviation "base_bits \ {base .. base + (2 ^ bits - 1)}" abbreviation "state' \ (s \ ksPSpace := \x. if base \ x \ x \ base + (2 ^ bits - 1) then None else ksPSpace s x \)" lemma ko_wp_at'[simp]: "\P p. (ko_wp_at' P p state') = (ko_wp_at' P p s \ p \ base_bits)" by (fastforce simp add: ko_wp_at_delete'[OF pd]) lemma obj_at'[simp]: "\P p. (obj_at' P p state') = (obj_at' P p s \ p \ base_bits)" by (fastforce simp add: obj_at'_real_def) lemma typ_at'[simp]: "\T p. (typ_at' P p state') = (typ_at' P p s \ p \ base_bits)" by (simp add: typ_at'_def) lemma valid_untyped[simp]: "s \' UntypedCap d base bits idx" using cte_wp_at_valid_objs_valid_cap' [OF cap valid_objs] by clarsimp lemma cte_wp_at'[simp]: "\P p. (cte_wp_at' P p state') = (cte_wp_at' P p s \ p \ base_bits)" by (fastforce simp:cte_wp_at_delete'[where idx = idx,OF valid_untyped pd ]) (* the bits of caps they need for validity argument are within their capRanges *) lemma valid_cap_ctes_pre: "\c. s \' c \ case c of CNodeCap ref bits g gs \ \x. ref + (x && mask bits) * 16 \ capRange c | Zombie ref (ZombieCNode bits) n \ \x. ref + (x && mask bits) * 16 \ capRange c | ArchObjectCap (PageTableCap ref data) \ \x < 0x100. ref + x * 4 \ capRange c | ArchObjectCap (PageDirectoryCap ref data) \ \x < 0x1000. ref + x * 4 \ capRange c | _ \ True" apply (drule valid_capAligned) apply (simp split: capability.split zombie_type.split arch_capability.split, safe) apply (clarsimp simp add: capRange_def capAligned_def objBits_simps pre_helper field_simps simp del: atLeastAtMost_iff) apply (clarsimp simp add: capRange_def capAligned_def simp del: atLeastAtMost_iff capBits.simps) apply (rule pre_helper2, simp_all)[1] apply (clarsimp simp add: capRange_def capAligned_def simp del: atLeastAtMost_iff capBits.simps) apply (rule pre_helper2, simp_all)[1] apply (clarsimp simp add: capRange_def capAligned_def objBits_simps pre_helper field_simps simp del: atLeastAtMost_iff) done lemma replycap_argument: "\p t m. cte_wp_at' (\cte. cteCap cte = ReplyCap t m) p s \ t \ {base .. base + (2 ^ bits - 1)}" using safe by (fastforce simp add: deletionIsSafe_def cte_wp_at_ctes_of field_simps) lemma valid_cap': "\p c. \ s \' c; cte_wp_at' (\cte. cteCap cte = c) p s; capRange c \ {base .. base + (2 ^ bits - 1)} = {} \ \ state' \' c" apply (subgoal_tac "capClass c = PhysicalClass \ capUntypedPtr c \ capRange c") apply (subgoal_tac "capClass c = PhysicalClass \ capUntypedPtr c \ {base .. base + (2 ^ bits - 1)}") apply (frule valid_cap_ctes_pre) apply (case_tac c, simp_all add: valid_cap'_def replycap_argument del: atLeastAtMost_iff split: zombie_type.split_asm) apply (simp add: field_simps del: atLeastAtMost_iff) apply blast apply (rename_tac arch_capability) apply (case_tac arch_capability, simp_all add: ARM_H.capUntypedPtr_def page_table_at'_def page_directory_at'_def shiftl_t2n del: atLeastAtMost_iff)[1] apply (rename_tac word vmrights vmpage_size option) apply (subgoal_tac "\p < 2 ^ (pageBitsForSize vmpage_size - pageBits). word + p * 2 ^ pageBits \ capRange c") apply blast apply (clarsimp simp: capRange_def capAligned_def) apply (frule word_less_power_trans2, rule pbfs_atleast_pageBits, simp add: word_bits_def) apply (rule context_conjI) apply (erule(1) is_aligned_no_wrap') apply (simp only: add_diff_eq[symmetric]) apply (rule word_plus_mono_right) apply simp apply (erule is_aligned_no_overflow') apply (simp add: field_simps del: atLeastAtMost_iff) apply blast apply (simp add: field_simps del: atLeastAtMost_iff) apply blast apply (simp add: valid_untyped'_def) apply (simp add: field_simps del: atLeastAtMost_iff) apply blast apply blast apply (clarsimp simp: capAligned_capUntypedPtr) done lemma objRefs_notrange: assumes asms: "ctes_of s p = Some c" "\ isUntypedCap (cteCap c)" shows "capRange (cteCap c) \ base_bits = {}" proof - from cap obtain node where ctes_of: "ctes_of s ptr = Some (CTE (UntypedCap d base bits idx) node)" apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte, simp) done show ?thesis using asms cap apply - apply (rule ccontr) apply (drule untyped_mdbD' [OF ctes_of _ _ _ _ umdb]) apply (simp add: isUntypedCap_def) apply (simp add: field_simps) apply assumption using nodesc apply (simp add:descendants_range'_def2) apply (drule(1) descendants_range_inD') apply (simp add:asms) apply (simp add:p_assoc_help) done qed lemma ctes_of_valid [elim!]: "ctes_of s p = Some cte \ s \' cteCap cte" by (case_tac cte, simp add: ctes_of_valid_cap' [OF _ valid_objs]) lemma valid_cap2: "\ cte_wp_at' (\cte. cteCap cte = c) p s \ \ state' \' c" apply (case_tac "isUntypedCap c") apply (drule cte_wp_at_valid_objs_valid_cap' [OF _ valid_objs]) apply (clarsimp simp: valid_cap'_def isCap_simps valid_untyped'_def) apply (rule valid_cap'[rotated], assumption) apply (clarsimp simp: cte_wp_at_ctes_of dest!: objRefs_notrange) apply (clarsimp simp: cte_wp_at_ctes_of) done lemma ex_nonz_cap_notRange: "ex_nonz_cap_to' p s \ p \ base_bits" apply (clarsimp simp: ex_nonz_cap_to'_def cte_wp_at_ctes_of) apply (case_tac "isUntypedCap (cteCap cte)") apply (clarsimp simp: isCap_simps) apply (drule subsetD[OF zobj_refs_capRange, rotated]) apply (rule valid_capAligned, erule ctes_of_valid) apply (drule(1) objRefs_notrange) apply (drule_tac a=p in equals0D) apply simp done lemma live_notRange: "\ ko_wp_at' P p s; \ko. P ko \ live' ko \ \ p \ base_bits" apply (drule if_live_then_nonz_capE' [OF iflive ko_wp_at'_weakenE]) apply simp apply (erule ex_nonz_cap_notRange) done lemma refs_notRange: "(x, tp) \ state_refs_of' s y \ y \ base_bits" apply (drule state_refs_of'_elemD) apply (erule live_notRange) apply (rule refs_of_live') apply clarsimp done lemma valid_obj': "\ valid_obj' obj s; ko_wp_at' (op = obj) p s \ \ valid_obj' obj state'" apply (case_tac obj, simp_all add: valid_obj'_def) apply (rename_tac endpoint) apply (case_tac endpoint, simp_all add: valid_ep'_def)[1] apply (clarsimp dest!: sym_refs_ko_wp_atD [OF _ sym_refs]) apply (drule(1) bspec)+ apply (clarsimp dest!: refs_notRange) apply (clarsimp dest!: sym_refs_ko_wp_atD [OF _ sym_refs]) apply (drule(1) bspec)+ apply (clarsimp dest!: refs_notRange) apply (rename_tac notification) apply (case_tac notification, simp_all add: valid_ntfn'_def valid_bound_tcb'_def)[1] apply (rename_tac ntfn bound) apply (case_tac ntfn, simp_all split:option.splits)[1] apply ((clarsimp dest!: sym_refs_ko_wp_atD [OF _ sym_refs] refs_notRange)+)[4] apply (drule(1) bspec)+ apply (clarsimp dest!: refs_notRange) apply (clarsimp dest!: sym_refs_ko_wp_atD [OF _ sym_refs] refs_notRange) apply (frule sym_refs_ko_wp_atD [OF _ sym_refs]) apply (clarsimp simp: valid_tcb'_def ko_wp_at'_def objBits_simps) apply (rule conjI) apply (erule ballEI, clarsimp elim!: ranE) apply (rule_tac p="p + x" in valid_cap2) apply (erule(2) cte_wp_at_tcbI') apply fastforce apply simp apply (rename_tac tcb) apply (case_tac "tcbState tcb", simp_all add: valid_tcb_state'_def valid_bound_ntfn'_def split:option.splits)[1] apply (clarsimp dest!: refs_notRange)+ apply (clarsimp simp: valid_cte'_def) apply (rule_tac p=p in valid_cap2) apply (clarsimp simp: ko_wp_at'_def objBits_simps cte_level_bits_def[symmetric]) apply (erule(2) cte_wp_at_cteI') apply simp apply (rename_tac arch_kernel_object) apply (case_tac "arch_kernel_object", simp_all) apply (rename_tac asidpool) apply (case_tac asidpool, clarsimp simp: page_directory_at'_def) apply (rename_tac pte) apply (case_tac pte, simp_all add: valid_mapping'_def) apply(rename_tac pde) apply (case_tac pde, simp_all add: valid_mapping'_def) done lemma st_tcb: "\P p. \ st_tcb_at' P p s; \ P Inactive; \ P IdleThreadState \ \ st_tcb_at' P p state'" by (fastforce simp: pred_tcb_at'_def obj_at'_real_def projectKOs dest: live_notRange) lemma irq_nodes_global: "\irq :: 10 word. irq_node' s + (ucast irq) * 16 \ global_refs' s" by (simp add: global_refs'_def mult.commute mult.left_commute) lemma global_refs: "global_refs' s \ base_bits = {}" using cap apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule valid_global_refsD' [OF _ refs]) apply (fastforce simp add: field_simps) done lemma global_refs2: "global_refs' s \ (- base_bits)" using global_refs by blast lemma irq_nodes_range: "\irq :: 10 word. irq_node' s + (ucast irq) * 16 \ base_bits" using irq_nodes_global global_refs by blast lemma cte_refs_notRange: assumes asms: "ctes_of s p = Some c" shows "cte_refs' (cteCap c) (irq_node' s) \ base_bits = {}" proof - from cap obtain node where ctes_of: "ctes_of s ptr = Some (CTE (UntypedCap d base bits idx) node)" apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte, simp) done show ?thesis using asms apply - apply (rule ccontr) apply (clarsimp elim!: nonemptyE) apply (frule ctes_of_valid) apply (frule valid_capAligned) apply (case_tac "\irq. cteCap c = IRQHandlerCap irq") apply (insert irq_nodes_range)[1] apply clarsimp apply (frule subsetD [OF cte_refs_capRange]) apply simp apply assumption apply (frule caps_containedD' [OF _ ctes_of _ _ contained]) apply (clarsimp dest!: isCapDs) apply (rule_tac x=x in notemptyI) apply (simp add: field_simps) apply (simp add: add_diff_eq[symmetric]) apply (drule objRefs_notrange) apply (clarsimp simp: isCap_simps) apply blast done qed lemma non_null_present: "cte_wp_at' (\c. cteCap c \ NullCap) p s \ p \ base_bits" apply (drule (1) if_unsafe_then_capD' [OF _ ifunsafe]) apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of dest!: cte_refs_notRange simp del: atLeastAtMost_iff) apply blast done lemma cte_cap: "ex_cte_cap_to' p s \ ex_cte_cap_to' p state'" apply (clarsimp simp: ex_cte_cap_to'_def) apply (frule non_null_present [OF cte_wp_at_weakenE']) apply clarsimp apply fastforce done lemma idle_notRange: "\cref. \ cte_wp_at' (\c. ksIdleThread s \ capRange (cteCap c)) cref s \ ksIdleThread s \ base_bits" apply (insert cap) apply (clarsimp simp: cte_wp_at_ctes_of) apply (erule_tac x=ptr in allE, clarsimp simp: field_simps) done abbreviation "ctes' \ map_to_ctes (\x. if base \ x \ x \ base + (2 ^ bits - 1) then None else ksPSpace s x)" lemmas tree_to_ctes = map_to_ctes_delete [OF valid_untyped pd] lemma map_to_ctesE[elim!]: "\ ctes' x = Some cte; \ ctes_of s x = Some cte; x \ base_bits \ \ P \ \ P" by (clarsimp simp: tree_to_ctes split: if_split_asm) lemma not_nullMDBNode: "\ ctes_of s x = Some cte; cteCap cte = NullCap; cteMDBNode cte = nullMDBNode \ P \ \ P" using nullcaps apply (cases cte) apply (simp add: valid_nullcaps_def) done lemma mdb_src: "\ ctes_of s \ x \ y; y \ 0 \ \ x \ base_bits" apply (rule non_null_present) apply (clarsimp simp: next_unfold' cte_wp_at_ctes_of) apply (erule(1) not_nullMDBNode) apply (simp add: nullMDBNode_def nullPointer_def) done lemma mdb_dest: "\ ctes_of s \ x \ y; y \ 0 \ \ y \ base_bits" apply (case_tac "x = 0") apply (insert no_0, simp add: next_unfold')[1] apply (drule(1) vdlist_nextD0 [OF _ _ dlist]) apply (rule non_null_present) apply (clarsimp simp: next_unfold' cte_wp_at_ctes_of mdb_prev_def) apply (erule(1) not_nullMDBNode) apply (simp add: nullMDBNode_def nullPointer_def) done lemma trancl_next[elim]: "\ ctes_of s \ x \\<^sup>+ y; x \ base_bits \ \ ctes' \ x \\<^sup>+ y" apply (erule rev_mp, erule converse_trancl_induct) apply clarsimp apply (rule r_into_trancl) apply (simp add: next_unfold' tree_to_ctes) apply clarsimp apply (rule_tac b=z in trancl_into_trancl2) apply (simp add: next_unfold' tree_to_ctes) apply (case_tac "z = 0") apply (insert no_0)[1] apply (erule tranclE2) apply (simp add: next_unfold') apply (simp add: next_unfold') apply (drule(1) mdb_dest) apply (simp add: next_unfold') done lemma mdb_parent_notrange: "ctes_of s \ x \ y \ x \ base_bits \ y \ base_bits" apply (erule subtree.induct) apply (frule(1) mdb_src, drule(1) mdb_dest, simp) apply (drule(1) mdb_dest, simp) done lemma mdb_parent: "ctes_of s \ x \ y \ ctes' \ x \ y" apply (erule subtree.induct) apply (frule(1) mdb_src, frule(1) mdb_dest) apply (rule subtree.direct_parent) apply (simp add: next_unfold' tree_to_ctes) apply assumption apply (simp add: parentOf_def tree_to_ctes) apply (frule(1) mdb_src, frule(1) mdb_dest) apply (erule subtree.trans_parent) apply (simp add: next_unfold' tree_to_ctes) apply assumption apply (frule mdb_parent_notrange) apply (simp add: parentOf_def tree_to_ctes) done lemma trancl_next_rev: "ctes' \ x \\<^sup>+ y \ ctes_of s \ x \\<^sup>+ y" apply (erule converse_trancl_induct) apply (rule r_into_trancl) apply (clarsimp simp: next_unfold') apply (rule_tac b=z in trancl_into_trancl2) apply (clarsimp simp: next_unfold') apply assumption done lemma is_chunk[elim!]: "is_chunk (ctes_of s) cap x y \ is_chunk ctes' cap x y" apply (simp add: is_chunk_def) apply (erule allEI) apply (clarsimp dest!: trancl_next_rev) apply (drule rtranclD, erule disjE) apply (clarsimp simp: tree_to_ctes) apply (cut_tac p=y in non_null_present) apply (clarsimp simp: cte_wp_at_ctes_of) apply simp apply (clarsimp dest!: trancl_next_rev simp: trancl_into_rtrancl) apply (clarsimp simp: tree_to_ctes) apply (cut_tac p=p'' in non_null_present) apply (clarsimp simp add: cte_wp_at_ctes_of) apply simp done lemma mdb_parent_rev: "ctes' \ x \ y \ ctes_of s \ x \ y" apply (erule subtree.induct) apply (rule subtree.direct_parent) apply (clarsimp simp: next_unfold' tree_to_ctes split: if_split_asm) apply assumption apply (clarsimp simp: parentOf_def tree_to_ctes split: if_split_asm) apply (erule subtree.trans_parent) apply (clarsimp simp: next_unfold' tree_to_ctes split: if_split_asm) apply assumption apply (clarsimp simp: parentOf_def tree_to_ctes split: if_split_asm) done end lemma exists_disj: "((\a. P a \ Q a)\(\a. P a \ Q' a)) = (\a. P a \ (Q a \ Q' a))" by auto lemma (in delete_locale) delete_invs': "invs' (ksMachineState_update (\ms. underlying_memory_update (\m x. if base \ x \ x \ base + (2 ^ bits - 1) then 0 else m x) ms) state')" (is "invs' (?state'')") using vds proof (simp add: invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def valid_mdb_ctes_def, safe) interpret Arch . (*FIXME: arch_split*) let ?s = state' let ?ran = base_bits show "pspace_aligned' ?s" using pa by (simp add: pspace_aligned'_def dom_def) show "pspace_distinct' ?s" using pd by (clarsimp simp add: pspace_distinct'_def ps_clear_def dom_if_None Diff_Int_distrib) show "valid_objs' ?s" using valid_objs apply (clarsimp simp: valid_objs'_def ran_def) apply (rule_tac p=a in valid_obj') apply fastforce apply (frule pspace_alignedD'[OF _ pa]) apply (frule pspace_distinctD'[OF _ pd]) apply (clarsimp simp: ko_wp_at'_def) done from sym_refs show "sym_refs (state_refs_of' ?s)" apply - apply (clarsimp simp: state_refs_ko_wp_at_eq elim!: rsubst[where P=sym_refs]) apply (rule ext) apply safe apply (simp add: refs_notRange[simplified] state_refs_ko_wp_at_eq) done from vq show "valid_queues ?s" apply (clarsimp simp: valid_queues_def bitmapQ_defs) apply (clarsimp simp: valid_queues_no_bitmap_def) apply (drule spec, drule spec, drule conjunct1, drule(1) bspec) apply (clarsimp simp: obj_at'_real_def) apply (frule if_live_then_nonz_capE'[OF iflive, OF ko_wp_at'_weakenE]) apply (clarsimp simp: projectKOs inQ_def) apply (clarsimp dest!: ex_nonz_cap_notRange) done from vq' show "valid_queues' ?s" by (simp add: valid_queues'_def) show "if_live_then_nonz_cap' ?s" using iflive apply (clarsimp simp: if_live_then_nonz_cap'_def) apply (drule spec, drule(1) mp) apply (clarsimp simp: ex_nonz_cap_to'_def) apply (rule exI, rule conjI, assumption) apply (drule non_null_present [OF cte_wp_at_weakenE']) apply clarsimp apply simp done from ifunsafe show "if_unsafe_then_cap' ?s" by (clarsimp simp: if_unsafe_then_cap'_def intro!: cte_cap) from idle_notRange refs have "ksIdleThread s \ ?ran" apply (simp add: cte_wp_at_ctes_of valid_global_refs'_def valid_refs'_def) apply blast done with idle show "valid_idle' ?s" apply (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def projectKOs) apply (clarsimp simp add: ps_clear_def dom_if_None Diff_Int_distrib) done from tcb_at_invs' [OF invs] ct_act show "cur_tcb' ?s" unfolding cur_tcb'_def apply (clarsimp simp: cur_tcb'_def ct_in_state'_def) apply (drule st_tcb) apply simp apply simp apply (simp add: pred_tcb_at'_def) done let ?ctes' = ctes' from no_0 show no_0': "no_0 ?ctes'" by (simp add: no_0_def tree_to_ctes) from dlist show "valid_dlist ?ctes'" apply (simp only: valid_dlist_def3) apply (rule conjI) apply (drule conjunct1) apply (elim allEI) apply (clarsimp simp: mdb_prev_def next_unfold' tree_to_ctes) apply (rule ccontr, clarsimp) apply (cut_tac p="mdbNext (cteMDBNode cte)" in non_null_present) apply (clarsimp simp: cte_wp_at_ctes_of) apply (erule(1) not_nullMDBNode) apply (simp add: nullMDBNode_def nullPointer_def no_0) apply simp apply (drule conjunct2) apply (elim allEI) apply (clarsimp simp: mdb_prev_def next_unfold' tree_to_ctes) apply (rule ccontr, clarsimp) apply (cut_tac p="mdbPrev (cteMDBNode z)" in non_null_present) apply (clarsimp simp: cte_wp_at_ctes_of) apply (erule(1) not_nullMDBNode) apply (simp add: nullMDBNode_def nullPointer_def no_0) apply simp done from chain_0 show "mdb_chain_0 ?ctes'" by (fastforce simp: mdb_chain_0_def Ball_def) from umdb show "untyped_mdb' ?ctes'" apply (simp add: untyped_mdb'_def) apply (erule allEI)+ apply (clarsimp simp: descendants_of'_def) apply (rule mdb_parent) apply (clarsimp simp: tree_to_ctes split: if_split_asm) done from badges show "valid_badges ?ctes'" by (simp add: valid_badges_def tree_to_ctes next_unfold') from contained show "caps_contained' ?ctes'" by (simp add: caps_contained'_def tree_to_ctes) from chunked show "mdb_chunked ?ctes'" apply (simp add: mdb_chunked_def) apply (elim allEI) apply clarsimp apply (intro conjI impI) apply (erule disjEI) apply fastforce apply fastforce apply (clarsimp dest!: trancl_next_rev) apply (clarsimp dest!: trancl_next_rev) done from uinc show "untyped_inc' ?ctes'" apply (simp add: untyped_inc'_def) apply (elim allEI) apply clarsimp apply (safe del: impCE, simp_all add: descendants_of'_def mdb_parent) done from nullcaps show "valid_nullcaps ?ctes'" by (clarsimp simp: valid_nullcaps_def) from ut_rev show "ut_revocable' ?ctes'" by (clarsimp simp: ut_revocable'_def) show "class_links ?ctes'" using clinks by (simp add: class_links_def tree_to_ctes mdb_next_unfold) show "valid_global_refs' ?s" using refs by (simp add: valid_global_refs'_def tree_to_ctes valid_cap_sizes'_def global_refs'_def valid_refs'_def ball_ran_eq) show "valid_arch_state' ?s" using arch global_refs2 apply (simp add: valid_arch_state'_def global_refs'_def) apply (intro conjI) apply (simp add: valid_asid_table'_def) apply (simp add: page_directory_at'_def page_directory_refs'_def subset_iff) apply (simp add: valid_global_pts'_def subset_iff page_table_at'_def page_table_refs'_def page_directory_at'_def) by fastforce show "valid_irq_node' (irq_node' s) ?s" using virq irq_nodes_range by (simp add: valid_irq_node'_def mult.commute mult.left_commute ucast_ucast_mask_8) show "valid_irq_handlers' ?s" using virqh apply (simp add: valid_irq_handlers'_def irq_issued'_def cteCaps_of_def tree_to_ctes Ball_def) apply (erule allEI) apply (clarsimp simp: ran_def) done from irq_ctrl show "irq_control ?ctes'" by (clarsimp simp: irq_control_def) from dist_z show "distinct_zombies ?ctes'" apply (simp add: tree_to_ctes distinct_zombies_def distinct_zombie_caps_def split del: if_split) apply (erule allEI, erule allEI) apply clarsimp done show "reply_masters_rvk_fb ?ctes'" using rep_r_fb by (simp add: tree_to_ctes reply_masters_rvk_fb_def ball_ran_eq) from virqs show "valid_irq_states' s" . from no_0_objs show "no_0_obj' state'" by (simp add: no_0_obj'_def) from pde_maps show "valid_pde_mappings' state'" by (simp add: valid_pde_mappings'_def) from irqs_masked show "irqs_masked' state'" by (simp add: irqs_masked'_def) from sa_simp ct_act show "sch_act_wf (ksSchedulerAction s) state'" apply (simp add: sch_act_simple_def) apply (case_tac "ksSchedulerAction s", simp_all add: ct_in_state'_def) apply (fastforce dest!: st_tcb elim!: pred_tcb'_weakenE) done from invs have "pspace_domain_valid s" by (simp add: invs'_def valid_state'_def) thus "pspace_domain_valid state'" by (simp add: pspace_domain_valid_def) from invs have "valid_machine_state' s" by (simp add: invs'_def valid_state'_def) thus "valid_machine_state' ?state''" apply (clarsimp simp: valid_machine_state'_def) apply (drule_tac x=p in spec) apply (simp add: pointerInUserData_def pointerInDeviceData_def typ_at'_def) apply (simp add: ko_wp_at'_def exists_disj) apply (elim exE conjE) apply (cut_tac ptr'=p in mask_in_range) apply fastforce using valid_untyped[simplified valid_cap'_def capability.simps] apply (simp add: valid_untyped'_def capAligned_def) apply (elim conjE) apply (drule_tac x="p && ~~ mask pageBits" in spec) apply (cut_tac x=p in is_aligned_neg_mask[of pageBits pageBits, simplified]) apply (clarsimp simp: mask_2pm1 ko_wp_at'_def obj_range'_def objBitsKO_def) apply (frule is_aligned_no_overflow'[of base bits]) apply (frule is_aligned_no_overflow'[of _ pageBits]) apply (frule (1) aligned_ranges_subset_or_disjoint [where n=bits and n'=pageBits]) apply (case_tac ko, simp_all add: objBits_simps) apply (auto simp add: x_power_minus_1) done from sa_simp ctnotinQ show "ct_not_inQ ?state''" apply (clarsimp simp: ct_not_inQ_def pred_tcb_at'_def) apply (drule obj_at'_and [THEN iffD2, OF conjI, OF ct_act [unfolded ct_in_state'_def pred_tcb_at'_def]]) apply (clarsimp simp: obj_at'_real_def) apply (frule if_live_then_nonz_capE'[OF iflive, OF ko_wp_at'_weakenE]) apply (clarsimp simp: projectKOs) apply (case_tac "tcbState obj") apply (clarsimp simp: projectKOs)+ apply (clarsimp dest!: ex_nonz_cap_notRange) done from ctcd show "ct_idle_or_in_cur_domain' ?state''" apply (simp add: ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def) apply (intro impI) apply (elim disjE impE) apply simp+ apply (intro impI) apply (rule disjI2) apply (drule obj_at'_and [THEN iffD2, OF conjI, OF ct_act [unfolded ct_in_state'_def st_tcb_at'_def]]) apply (clarsimp simp: obj_at'_real_def) apply (frule if_live_then_nonz_capE'[OF iflive, OF ko_wp_at'_weakenE]) apply (clarsimp simp: projectKOs) apply (case_tac "tcbState obj") apply (clarsimp simp: projectKOs)+ apply (clarsimp dest!: ex_nonz_cap_notRange elim!: ko_wp_at'_weakenE) done from cdm show "ksCurDomain s \ maxDomain" . from invs have urz: "untyped_ranges_zero' s" by (simp add: invs'_def valid_state'_def) show "untyped_ranges_zero_inv (cteCaps_of state') (gsUntypedZeroRanges s)" apply (simp add: untyped_zero_ranges_cte_def urz[unfolded untyped_zero_ranges_cte_def, rule_format, symmetric]) apply (clarsimp simp: fun_eq_iff intro!: arg_cong[where f=Ex]) apply safe apply (drule non_null_present[OF cte_wp_at_weakenE']) apply (clarsimp simp: untypedZeroRange_def) apply simp done qed (clarsimp) lemma (in delete_locale) delete_ko_wp_at': assumes objs: "ko_wp_at' P p s \ ex_nonz_cap_to' p s" shows "ko_wp_at' P p state'" using objs by (clarsimp simp: ko_wp_at'_def ps_clear_def dom_if_None Diff_Int_distrib dest!: ex_nonz_cap_notRange) lemma (in delete_locale) null_filter': assumes descs: "Q (null_filter' (ctes_of s))" shows "Q (null_filter' (ctes_of state'))" using descs ifunsafe apply (clarsimp elim!: rsubst[where P=Q]) apply (rule ext) apply (clarsimp simp:null_filter'_def tree_to_ctes) apply (rule ccontr) apply (clarsimp) apply (cut_tac p = x in non_null_present) apply (simp add:cte_wp_at_ctes_of) apply (rule ccontr) apply simp apply (erule(1) not_nullMDBNode) apply (case_tac y,simp) apply simp done lemma (in delete_locale) delete_ex_cte_cap_to': assumes exc: "ex_cte_cap_to' p s" shows "ex_cte_cap_to' p state'" using exc by (clarsimp elim!: cte_cap) lemma deleteObjects_null_filter: "\cte_wp_at' (\c. cteCap c = UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s)) and (\s. P (null_filter' (ctes_of s))) and K (bits < word_bits \ is_aligned ptr bits)\ deleteObjects ptr bits \\rv s. P (null_filter' (ctes_of s))\" apply (simp add: deleteObjects_def3) apply (simp add: deleteObjects_def3 doMachineOp_def split_def) apply wp apply clarsimp apply (subgoal_tac "delete_locale s ptr bits p idx d") apply (drule_tac Q = P in delete_locale.null_filter') apply assumption apply (clarsimp simp:p_assoc_help) apply (simp add: eq_commute field_simps) apply (subgoal_tac "ksPSpace (s\ksMachineState := snd ((), b)\) = ksPSpace s", simp only:, simp) apply (unfold_locales, simp_all) done lemma deleteObjects_descendants: "\cte_wp_at' (\c. cteCap c = UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s)) and (\s. descendants_range_in' H p (ctes_of s)) and K (bits < word_bits \ is_aligned ptr bits)\ deleteObjects ptr bits \\rv s. descendants_range_in' H p (ctes_of s)\" apply (simp add:descendants_range_in'_def2) apply (wp deleteObjects_null_filter) apply fastforce done lemma dmo'_ksPSpace_update_comm: assumes "empty_fail f" shows "doMachineOp f >>= (\s. modify (ksPSpace_update g)) = modify (ksPSpace_update g) >>= (\s. doMachineOp f)" proof - have ksMachineState_ksPSpace_update: "\s. ksMachineState (ksPSpace_update g s) = ksMachineState s" by simp have updates_independent: "\f. ksPSpace_update g \ ksMachineState_update f = ksMachineState_update f \ ksPSpace_update g" by (rule ext) simp from assms show ?thesis apply (simp add: doMachineOp_def split_def bind_assoc) apply (simp add: gets_modify_comm2[OF ksMachineState_ksPSpace_update]) apply (rule arg_cong2[where f=bind, OF refl], rule ext) apply (simp add: empty_fail_def select_f_walk[OF empty_fail_modify] modify_modify updates_independent) done qed lemma doMachineOp_modify: "doMachineOp (modify g) = modify (ksMachineState_update g)" apply (simp add: doMachineOp_def split_def select_f_returns) apply (rule ext) apply (simp add: simpler_gets_def simpler_modify_def bind_def) done context begin interpretation Arch . (*FIXME: arch_split*) lemma deleteObjects_invs': "\cte_wp_at' (\c. cteCap c = UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \ is_aligned ptr bits)\ deleteObjects ptr bits \\rv. invs'\" proof - show ?thesis apply (rule hoare_pre) apply (rule_tac G="is_aligned ptr bits \ 2 \ bits \ bits \ word_bits" in hoare_grab_asm) apply (clarsimp simp add: deleteObjects_def2) apply (simp add: freeMemory_def bind_assoc doMachineOp_bind ef_storeWord) apply (simp add: bind_assoc[where f="\_. modify f" for f, symmetric]) apply (simp add: word_size_def mapM_x_storeWord_step doMachineOp_modify modify_modify) apply (simp add: bind_assoc intvl_range_conv'[where 'a=32, folded word_bits_def] mask_def field_simps) apply (wp) apply (simp cong: if_cong) apply (subgoal_tac "is_aligned ptr bits \ 2 \ bits \ bits < word_bits",simp) apply clarsimp apply (frule(2) delete_locale.intro, simp_all)[1] apply (rule subst[rotated, where P=invs'], erule delete_locale.delete_invs') apply (simp add: field_simps) apply clarsimp apply (drule invs_valid_objs') apply (drule (1) cte_wp_at_valid_objs_valid_cap') apply (clarsimp simp add: valid_cap'_def capAligned_def) done qed lemma deleteObjects_st_tcb_at': "\cte_wp_at' (\c. cteCap c = UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s)) and st_tcb_at' (P and op \ Inactive and op \ IdleThreadState) t and K (bits < word_bits \ is_aligned ptr bits)\ deleteObjects ptr bits \\rv. st_tcb_at' P t\" apply (simp add: deleteObjects_def3 doMachineOp_def split_def) apply wp apply clarsimp apply (subgoal_tac "delete_locale s ptr bits p idx d") apply (drule delete_locale.delete_ko_wp_at' [where p = t and P="case_option False (P \ tcbState) \ projectKO_opt", simplified eq_commute]) apply (simp add: pred_tcb_at'_def obj_at'_real_def) apply (rule conjI) apply (fastforce elim: ko_wp_at'_weakenE) apply (erule if_live_then_nonz_capD' [rotated]) apply (clarsimp simp: projectKOs) apply (clarsimp simp: invs'_def valid_state'_def) apply (clarsimp simp: pred_tcb_at'_def obj_at'_real_def field_simps ko_wp_at'_def ps_clear_def cong:if_cong split: option.splits) apply (simp add: delete_locale_def) done lemma ex_cte_cap_wp_to'_gsCNodes_update[simp]: "ex_cte_cap_wp_to' P p (gsCNodes_update f s') = ex_cte_cap_wp_to' P p s'" by (simp add: ex_cte_cap_wp_to'_def) lemma ex_cte_cap_wp_to'_gsUserPages_update[simp]: "ex_cte_cap_wp_to' P p (gsUserPages_update f s') = ex_cte_cap_wp_to' P p s'" by (simp add: ex_cte_cap_wp_to'_def) lemma deleteObjects_cap_to': "\cte_wp_at' (\c. cteCap c = UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s)) and ex_cte_cap_to' p' and K (bits < word_bits \ is_aligned ptr bits)\ deleteObjects ptr bits \\rv. ex_cte_cap_to' p'\" apply (simp add: deleteObjects_def3 doMachineOp_def split_def) apply wp apply clarsimp apply (subgoal_tac "delete_locale s ptr bits p idx d") apply (drule delete_locale.delete_ex_cte_cap_to', assumption) apply (simp cong:if_cong) apply (subgoal_tac "s\ksMachineState := b, ksPSpace := \x. if ptr \ x \ x \ ptr + 2 ^ bits - 1 then None else ksPSpace s x\ = ksMachineState_update (\_. b) (s\ksPSpace := \x. if ptr \ x \ x \ ptr + 2 ^ bits - 1 then None else ksPSpace s x\)",erule ssubst) apply (simp add: field_simps ex_cte_cap_wp_to'_def cong:if_cong) apply simp apply (simp add: delete_locale_def) done lemma valid_untyped_no_overlap: "\ valid_untyped' d ptr bits idx s; is_aligned ptr bits; valid_pspace' s \ \ pspace_no_overlap' ptr bits (s\ksPSpace := ksPSpace s |` (- {ptr .. ptr + 2 ^ bits - 1})\)" apply (clarsimp simp del: atLeastAtMost_iff simp: pspace_no_overlap'_def valid_cap'_def valid_untyped'_def is_aligned_neg_mask_eq) apply (drule_tac x=x in spec) apply (drule restrict_map_Some_iff[THEN iffD1]) apply clarsimp apply (frule pspace_alignedD') apply (simp add: valid_pspace'_def) apply (frule pspace_distinctD') apply (simp add: valid_pspace'_def) apply (unfold ko_wp_at'_def obj_range'_def) apply (drule (1) aligned_ranges_subset_or_disjoint) apply (clarsimp simp del: Int_atLeastAtMost atLeastAtMost_iff atLeastatMost_subset_iff) apply (elim disjE) apply (subgoal_tac "ptr \ {x..x + 2 ^ objBitsKO ko - 1}") apply (clarsimp simp:p_assoc_help) apply (clarsimp simp:p_assoc_help) apply fastforce+ done lemma pspace_no_overlap'_gsCNodes_update[simp]: "pspace_no_overlap' p b (gsCNodes_update f s') = pspace_no_overlap' p b s'" by (simp add: pspace_no_overlap'_def) lemma pspace_no_overlap'_gsUserPages_update[simp]: "pspace_no_overlap' p b (gsUserPages_update f s') = pspace_no_overlap' p b s'" by (simp add: pspace_no_overlap'_def) lemma pspace_no_overlap'_ksMachineState_update[simp]: "pspace_no_overlap' p n (ksMachineState_update f s) = pspace_no_overlap' p n s" by (simp add: pspace_no_overlap'_def) lemma deleteObject_no_overlap[wp]: "\valid_cap' (UntypedCap d ptr bits idx) and valid_pspace'\ deleteObjects ptr bits \\rv s. pspace_no_overlap' ptr bits s\" apply (simp add: deleteObjects_def3 doMachineOp_def split_def) apply wp apply (clarsimp simp: valid_cap'_def cong:if_cong) apply (drule (2) valid_untyped_no_overlap) apply (subgoal_tac "s\ksMachineState := b, ksPSpace := \x. if ptr \ x \ x \ ptr + 2 ^ bits - 1 then None else ksPSpace s x\ = ksMachineState_update (\_. b) (s\ksPSpace := ksPSpace s |` (- {ptr..ptr + 2 ^ bits - 1})\)", simp) apply (case_tac s, simp) apply (rule ext) apply simp done lemma deleteObjects_cte_wp_at': "\\s. cte_wp_at' P p s \ p \ {ptr .. ptr + 2 ^ bits - 1} \ s \' (UntypedCap d ptr bits idx) \ valid_pspace' s\ deleteObjects ptr bits \\rv s. cte_wp_at' P p s\" apply (simp add: deleteObjects_def3 doMachineOp_def split_def) apply wp apply (clarsimp simp: valid_pspace'_def cong:if_cong) apply (subgoal_tac "s\ksMachineState := b, ksPSpace := \x. if ptr \ x \ x \ ptr + 2 ^ bits - 1 then None else ksPSpace s x\ = ksMachineState_update (\_. b) (s\ksPSpace := \x. if ptr \ x \ x \ ptr + 2 ^ bits - 1 then None else ksPSpace s x\)", erule ssubst) apply (simp add: cte_wp_at_delete' x_power_minus_1) apply (case_tac s, simp) done lemma deleteObjects_invs_derivatives: "\cte_wp_at' (\c. cteCap c = UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \ is_aligned ptr bits)\ deleteObjects ptr bits \\rv. valid_pspace'\" "\cte_wp_at' (\c. cteCap c = UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \ is_aligned ptr bits)\ deleteObjects ptr bits \\rv. valid_mdb'\" "\cte_wp_at' (\c. cteCap c = UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \ is_aligned ptr bits)\ deleteObjects ptr bits \\rv. pspace_aligned'\" "\cte_wp_at' (\c. cteCap c = UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \ is_aligned ptr bits)\ deleteObjects ptr bits \\rv. pspace_distinct'\" by (safe intro!: hoare_strengthen_post [OF deleteObjects_invs']) lemma deleteObjects_nosch: "\\s. P (ksSchedulerAction s)\ deleteObjects ptr sz \\rv s. P (ksSchedulerAction s)\" by (simp add: deleteObjects_def3 | wp hoare_drop_imp)+ lemma deleteObjects_valid_arch_state': "\cte_wp_at' (\c. cteCap c = UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \ is_aligned ptr bits)\ deleteObjects ptr bits \\rv. valid_arch_state'\" by (safe intro!: hoare_strengthen_post [OF deleteObjects_invs']) (* Prooving the reordering here *) lemma createObjects'_wp_subst: "\\P\createObjects a b c d\\r. Q\\ \ \P\createObjects' a b c d\\r. Q\" apply (clarsimp simp:createObjects_def valid_def return_def bind_def) apply (drule_tac x = s in spec) apply (clarsimp simp:split_def) apply auto done definition pspace_no_overlap_cell' where "pspace_no_overlap_cell' p \ \kh. \x ko. kh x = Some ko \ p \ {x..x + (2 ^ objBitsKO ko - 1)}" lemma pspace_no_overlap_cellD': "\ksPSpace s x = Some ko; pspace_no_overlap_cell' p (ksPSpace s)\ \ p \ {x..x + (2 ^ objBitsKO ko - 1)}" by(auto simp:pspace_no_overlap_cell'_def) lemma pspace_no_overlap'_lift: assumes typ_at:"\slot P Q. \\s. P (typ_at' Q slot s)\ f \\r s. P (typ_at' Q slot s) \" assumes ps :"\Q\ f \\r s. pspace_aligned' s \ pspace_distinct' s \" shows "\Q and pspace_no_overlap' ptr sz \ f \\r. pspace_no_overlap' ptr sz\" proof - note 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 show ?thesis apply (clarsimp simp:valid_def pspace_no_overlap'_def) apply (drule_tac x = x in spec) apply (subgoal_tac "\ko'. ksPSpace s x = Some ko' \ koTypeOf ko = koTypeOf ko'") apply (clarsimp dest!:objBits_type) apply (rule ccontr) apply clarsimp apply (frule_tac slot1 = x and Q1 = "koTypeOf ko" and P1 = "\a. \ a" in use_valid[OF _ typ_at]) apply (clarsimp simp:typ_at'_def ko_wp_at'_def)+ apply (frule(1) use_valid[OF _ ps]) apply (clarsimp simp:valid_pspace'_def) apply (frule(1) pspace_alignedD') apply (drule(1) pspace_distinctD') apply simp done qed lemma setCTE_pspace_no_overlap': "\pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz\ setCTE cte src \\r. pspace_no_overlap' ptr sz\" apply (rule pspace_no_overlap'_lift) apply (wp setCTE_typ_at') apply auto done lemma getCTE_commute: assumes cte_at_modify: "\Q. \\s. P s \ cte_wp_at' Q dest s \ f \\a s. cte_wp_at' Q dest s\" shows "monad_commute (P and cte_at' dest) (getCTE dest) f" proof - have getsame: "\x y s. (x,y)\ fst (getCTE dest s) \ y = s" apply (drule use_valid) prefer 3 apply (simp|wp)+ done show ?thesis apply (simp add:monad_commute_def bind_assoc getCTE_def split_def cte_at'_def) apply (clarsimp simp:bind_def split_def return_def) apply (rule conjI) apply (rule set_eqI) apply (rule iffI) apply clarsimp apply (rule bexI[rotated], assumption) apply (drule_tac Q1 ="op = cte" in use_valid[OF _ cte_at_modify]) apply (simp add:cte_wp_at'_def) apply (simp add:cte_wp_at'_def) apply clarsimp apply (rule conjI) apply (frule_tac Q1 = "op = cte" in use_valid[OF _ cte_at_modify]) apply (clarsimp simp:cte_wp_at'_def ko_wp_at'_def) apply (clarsimp simp:cte_wp_at'_def) apply (rule bexI[rotated], assumption) apply (metis fst_eqD getObject_cte_det snd_eqD) apply (cut_tac no_failD[OF no_fail_getCTE[unfolded getCTE_def]]) prefer 2 apply (simp add:cte_wp_at'_def) apply fastforce apply simp apply (rule iffI) apply clarsimp+ apply (cut_tac s = b in no_failD[OF no_fail_getCTE[unfolded getCTE_def]]) prefer 2 apply fastforce apply (drule_tac Q1 = "op = cte" in use_valid[OF _ cte_at_modify]) apply (simp add:cte_wp_at'_def) apply (simp add:cte_wp_at_ctes_of) done qed definition "cte_check \ \b src a next. (case b of KOTCB tcb \ (is_aligned a (objBits tcb) \ (case next of None \ True | Some z \ 2^(objBits tcb) \ z - a)) \ (src - a = tcbVTableSlot << cteSizeBits \ src - a = tcbCTableSlot << cteSizeBits \ src - a = tcbReplySlot << cteSizeBits \ src - a = tcbCallerSlot << cteSizeBits \ src - a = tcbIPCBufferSlot << cteSizeBits ) | KOCTE v1 \ ( src = a \ (is_aligned a (objBits (makeObject::cte))) \ (case next of None \ True | Some z \ 2^(objBits (makeObject::cte)) \ z - a)) | _ \ False)" definition locateCTE where "locateCTE src \ (do ps \ gets ksPSpace; (before, after) \ return (lookupAround2 src ps); (ptr,val) \ maybeToMonad before; assert (cte_check val src ptr after); return ptr od)" definition cte_update where "cte_update \ \cte b src a. (case b of KOTCB tcb \ if (src - a = tcbVTableSlot << cteSizeBits) then KOTCB (tcbVTable_update (\_. cte) tcb) else if (src - a = tcbCTableSlot << cteSizeBits) then KOTCB (tcbCTable_update (\_. cte) tcb) else if (src - a = tcbReplySlot << cteSizeBits) then KOTCB (tcbReply_update (\_. cte) tcb) else if (src - a = tcbCallerSlot << cteSizeBits) then KOTCB (tcbCaller_update (\_. cte) tcb) else if (src - a = tcbIPCBufferSlot << cteSizeBits) then KOTCB (tcbIPCBufferFrame_update (\_. cte) tcb) else KOTCB tcb | KOCTE v1 \ KOCTE cte | x \ x)" lemma cte_check_range: "cte_check val src ptr (snd (lookupAround2 src (ksPSpace s))) \ src \ {ptr .. ptr + 2^objBitsKO val - 1}" apply (case_tac val) apply (simp_all add:cte_check_def) apply (clarsimp simp: tcbVTableSlot_def cteSizeBits_def tcbCTableSlot_def tcbReplySlot_def tcbCallerSlot_def tcbIPCBufferSlot_def) apply (intro conjI) apply (elim disjE) apply (clarsimp simp:field_simps objBits_simps |erule is_aligned_no_wrap')+ apply (elim disjE) apply (clarsimp simp:field_simps objBits_simps |erule is_aligned_no_wrap' | rule word_plus_mono_right)+ done lemma simpler_updateObject_def: "updateObject (cte::cte) b src a next = (\s. (if (cte_check b src a next) then ({(cte_update cte b src a,s)}, False) else fail s))" apply (rule ext) apply (clarsimp simp:ObjectInstances_H.updateObject_cte objBits_simps) apply (case_tac b) apply (simp_all add:cte_check_def typeError_def fail_def tcbIPCBufferSlot_def tcbCallerSlot_def tcbReplySlot_def tcbCTableSlot_def tcbVTableSlot_def) by (intro conjI impI; clarsimp simp:alignCheck_def unless_def when_def not_less[symmetric] alignError_def is_aligned_mask magnitudeCheck_def cte_update_def return_def tcbIPCBufferSlot_def tcbCallerSlot_def tcbReplySlot_def tcbCTableSlot_def tcbVTableSlot_def objBits_simps cteSizeBits_def split:option.splits; fastforce simp:return_def fail_def bind_def)+ lemma setCTE_def2: "(setCTE src cte) = (do ptr \ locateCTE src; modify (ksPSpace_update (\ps. ps(ptr \ (cte_update cte (the (ps ptr)) src ptr )))) od)" apply (clarsimp simp:setCTE_def setObject_def split_def locateCTE_def bind_assoc) apply (rule ext) apply (rule_tac Q = "\r s'. s'= x \ r = ksPSpace x " in monad_eq_split) apply (rule_tac Q = "\ptr s'. s' = x \ snd ptr = the ((ksPSpace x) (fst ptr) ) " in monad_eq_split) apply (clarsimp simp:assert_def return_def fail_def bind_def simpler_modify_def) apply (clarsimp simp:simpler_updateObject_def fail_def) apply (wp|clarsimp simp:)+ apply (simp add:lookupAround2_char1) apply wp apply simp done lemma pspace_distinctD2': "\ksPSpace s a = Some b; z \ obj_range' a b; pspace_distinct' s \ \ ksPSpace s z = (if (z = a) then Some b else None)" apply (clarsimp simp: pspace_distinct'_def ps_clear_def) apply (rule ccontr) apply (clarsimp) apply (drule_tac x = a in bspec) apply fastforce apply (erule_tac x = z in in_empty_interE) apply (clarsimp simp:obj_range'_def) apply clarsimp done lemma pspace_no_overlapD3': "\pspace_no_overlap' ptr sz s;ksPSpace s p = Some obj;is_aligned ptr sz\ \ obj_range' p obj \ {ptr..ptr + 2 ^ sz - 1} = {}" apply (unfold pspace_no_overlap'_def) apply (drule spec)+ apply (erule(1) impE) apply (simp only:is_aligned_neg_mask_eq obj_range'_def p_assoc_help) done lemma singleton_locateCTE: "a \ fst (locateCTE src s) = ({a} = fst (locateCTE src s))" apply (clarsimp simp:locateCTE_def assert_opt_def assert_def gets_def get_def bind_def return_def split_def) apply (clarsimp simp:return_def fail_def split:if_splits option.splits)+ done lemma locateCTE_inv: "\P\locateCTE s\\r. P\" apply (simp add:locateCTE_def split_def) apply wp apply clarsimp done lemma locateCTE_case: "\\\ locateCTE src \\r s. \obj. ksPSpace s r = Some obj \ (case obj of KOTCB tcb \ True | KOCTE v \ True | _ \ False)\" apply (clarsimp simp:locateCTE_def split_def | wp)+ apply (clarsimp simp: lookupAround2_char1) apply (case_tac b) apply (simp_all add:cte_check_def) done lemma cte_wp_at_top: "(cte_wp_at' \ src s) = (\a b. ( fst (lookupAround2 src (ksPSpace s)) = Some (a, b) \ cte_check b src a (snd (lookupAround2 src (ksPSpace s)))))" apply (simp add:cte_wp_at'_def getObject_def gets_def get_def bind_def return_def split_def assert_opt_def fail_def split:option.splits) apply (clarsimp simp:loadObject_cte) apply (case_tac b,simp_all) apply ((simp add: typeError_def fail_def cte_check_def split: Structures_H.kernel_object.splits)+)[5] apply (simp add:loadObject_cte cte_check_def tcbIPCBufferSlot_def tcbCallerSlot_def tcbReplySlot_def tcbCTableSlot_def tcbVTableSlot_def objBits_simps cteSizeBits_def) apply (simp add:alignCheck_def bind_def alignError_def fail_def return_def objBits_simps magnitudeCheck_def in_monad is_aligned_mask when_def split:option.splits) apply (intro conjI impI allI,simp_all add:not_le) apply (clarsimp simp:cte_check_def) apply (simp add:alignCheck_def bind_def alignError_def fail_def return_def objBits_simps magnitudeCheck_def in_monad is_aligned_mask when_def split:option.splits) apply (intro conjI impI allI,simp_all add:not_le) apply (simp add:typeError_def fail_def cte_check_def split:Structures_H.kernel_object.splits)+ done lemma neq_out_intv: "\a \ b; b \ {a..a + c - 1} - {a} \ \ b \ {a..a + c - 1}" by simp lemma rule_out_intv: "\ ksPSpace s a = Some obj; ksPSpace s b = Some obj'; pspace_distinct' s; a\b \ \ b \ {a..a + 2 ^ objBitsKO obj - 1}" apply (drule(1) pspace_distinctD') apply (subst (asm) ps_clear_def) apply (drule_tac x = b in orthD2) apply fastforce apply (drule neq_out_intv) apply simp apply simp done lemma locateCTE_monad: assumes ko_wp_at: "\Q dest. \\s. P1 s \ ko_wp_at' (\obj. Q (objBitsKO obj)) dest s \ f \\a s. ko_wp_at' (\obj. Q (objBitsKO obj)) dest s\" assumes cte_wp_at: "\ dest. \\s. P2 s \ cte_wp_at' \ dest s \ f \\a s. cte_wp_at' \ dest s\" assumes psp_distinct: "\\s. P3 s \ f \\a s. pspace_distinct' s\" assumes psp_aligned: "\\s. P4 s \ f \\a s. pspace_aligned' s\" shows "\{(ptr, s)} = fst (locateCTE src s); (r, s') \ fst (f s);pspace_aligned' s;pspace_distinct' s;(P1 and P2 and P3 and P4) s\ \ {(ptr,s')} = fst (locateCTE src s')" proof - have src_in_range: "\obj src a m s'. \cte_check obj src a m;ksPSpace s' a = Some obj\ \ src \ {a..a + 2 ^ objBitsKO obj - 1}" proof - fix obj src a m show "\s'. \cte_check obj src a m; ksPSpace s' a = Some obj\ \ src \ {a..a + 2 ^ objBitsKO obj - 1}" apply (case_tac obj) apply (simp_all add:cte_check_def cteSizeBits_def) apply (clarsimp simp add:objBits_simps) apply (elim disjE) apply (simp add: tcbVTableSlot_def field_simps word_plus_mono_right tcbCTableSlot_def tcbReplySlot_def tcbCallerSlot_def tcbIPCBufferSlot_def is_aligned_no_wrap'[where sz = 9 and ptr = a and off = "0x1FF",simplified] is_aligned_no_wrap'[where sz = 9 and ptr = a and off = "0x10",simplified] is_aligned_no_wrap'[where sz = 9 and ptr = a and off = "0x20",simplified] is_aligned_no_wrap'[where sz = 9 and ptr = a and off = "0x30",simplified] is_aligned_no_wrap'[where sz = 9 and ptr = a and off = "0x40",simplified])+ apply (clarsimp simp add:objBits_simps field_simps) apply (erule is_aligned_no_wrap',simp) done qed note blah[simp del] = usableUntypedRange.simps atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex have step1: "\(ptr, s) \ fst (locateCTE src s); (r, s') \ fst (f s); pspace_aligned' s; pspace_distinct' s; (P1 and P2 and P3 and P4) s\ \ (ptr,s') \ fst (locateCTE src s')" apply (frule use_valid[OF _ locateCTE_case]) apply simp apply (clarsimp simp: locateCTE_def gets_def split_def get_def bind_def return_def assert_opt_def fail_def assert_def split: option.splits if_split_asm) apply (frule_tac dest1 = src in use_valid[OF _ cte_wp_at]) apply simp apply (subst cte_wp_at_top) apply simp apply (clarsimp simp add:cte_wp_at_top) apply (clarsimp simp:lookupAround2_char1) apply (frule_tac dest1 = ptr and Q1 = "\x. x = objBitsKO b" in use_valid[OF _ ko_wp_at]) apply (frule(1) pspace_alignedD') apply (frule(1) pspace_distinctD') apply (auto simp add:ko_wp_at'_def)[1] apply (clarsimp simp add:ko_wp_at'_def) apply (rule ccontr) apply (frule use_valid[OF _ psp_distinct]) apply simp apply (frule use_valid[OF _ psp_aligned]) apply simp apply (frule_tac x = a in pspace_distinctD') apply simp apply (frule_tac s = s' and a = ptr in rule_out_intv[rotated]) apply simp+ apply (frule_tac s = s' and b = ptr and a = a in rule_out_intv) apply simp+ apply (thin_tac "\x. P x \ Q x" for P Q)+ apply (drule_tac p = ptr and p' = a in aligned_ranges_subset_or_disjoint) apply (erule(1) pspace_alignedD') apply (drule(1) src_in_range)+ apply (drule base_member_set[OF pspace_alignedD']) apply simp apply (simp add:objBitsKO_bounded2[unfolded word_bits_def,simplified]) apply (drule base_member_set[OF pspace_alignedD']) apply simp apply (simp add:objBitsKO_bounded2[unfolded word_bits_def,simplified]) apply (clarsimp simp:field_simps) apply blast done assume "{(ptr, s)} = fst (locateCTE src s)" "(r, s') \ fst (f s)" "pspace_aligned' s" "pspace_distinct' s" "(P1 and P2 and P3 and P4) s" thus ?thesis using assms step1 by (clarsimp simp:singleton_locateCTE) qed lemma empty_fail_locateCTE: "empty_fail (locateCTE src)" by (simp add:locateCTE_def bind_assoc split_def) lemma fail_empty_locateCTE: "snd (locateCTE src s) \ fst (locateCTE src s) = {}" by (auto simp: assert_def fail_def locateCTE_def bind_assoc return_def split_def gets_def get_def bind_def assert_opt_def image_def split:option.splits if_split_asm)+ lemma locateCTE_commute: assumes nf: "no_fail P0 f" "no_fail P1 (locateCTE src)" and psp_distinct: "\\s. P2 s \ f \\a s. pspace_distinct' s\" and psp_aligned: "\\s. P3 s \ f \\a s. pspace_aligned' s\" assumes ko_wp_at: "\Q dest. \\s. (P0 and P1 and P2 and P3) s \ ko_wp_at' (\obj. Q (objBitsKO obj)) dest s \ f \\a s. ko_wp_at' (\obj. Q (objBitsKO obj)) dest s\" and cte_wp_at: "\ dest. \\s. (P0 and P1 and P2 and P3) s \ cte_wp_at' \ dest s \ f \\a s. cte_wp_at' \ dest s\" shows "monad_commute (P0 and P1 and P2 and P3 and P4 and P5 and pspace_aligned' and pspace_distinct') (locateCTE src) f" proof - have same: "\ptr val next s s'. (ptr, s') \ fst (locateCTE src s) \ s' = s" by (erule use_valid[OF _ locateCTE_inv],simp) show ?thesis apply (clarsimp simp:monad_commute_def) apply (clarsimp simp:bind_def return_def) apply (intro conjI iffI set_eqI) apply (clarsimp) apply (frule same) apply (clarsimp) apply (rule bexI[rotated], assumption) apply (frule singleton_locateCTE[THEN iffD1]) apply (frule locateCTE_monad [OF ko_wp_at cte_wp_at psp_distinct psp_aligned]) apply assumption+ apply simp apply (clarsimp) apply (rule bexI[rotated]) apply (fastforce) apply clarsimp apply clarsimp apply (frule empty_failD2[OF empty_fail_locateCTE no_failD[OF nf(2)]]) apply clarsimp apply (rule bexI[rotated],assumption) apply (clarsimp) apply (frule_tac s = bb in same) apply (frule_tac s = s in same) apply clarsimp apply (frule_tac s1 = s in singleton_locateCTE[THEN iffD1]) apply (frule locateCTE_monad [OF ko_wp_at cte_wp_at psp_distinct psp_aligned]) apply assumption+ apply simp apply (rule bexI[rotated],assumption) apply (drule sym) apply (clarsimp simp:singleton_locateCTE singleton_iff) apply fastforce apply (clarsimp simp:split_def image_def) apply (elim disjE) apply clarsimp apply (drule same) apply simp apply (frule no_failD[OF nf(2)]) apply simp apply (clarsimp simp:split_def image_def) apply (elim disjE) apply clarsimp apply (frule empty_failD2[OF empty_fail_locateCTE no_failD[OF nf(2)]]) apply clarsimp apply (frule same) apply simp apply (frule singleton_locateCTE[THEN iffD1]) apply (frule locateCTE_monad [OF ko_wp_at cte_wp_at psp_distinct psp_aligned]) apply assumption+ apply simp apply (clarsimp) apply (simp add: fail_empty_locateCTE) apply (simp add: no_failD[OF nf(1)]) done qed lemmas getObjSize_simps = ARM_H.getObjectSize_def[split_simps ARM_H.object_type.split apiobject_type.split] lemma arch_toAPIType_simps: "ARM_H.toAPIType ty = Some a \ ty = APIObjectType a" by (case_tac ty,auto simp:ARM_H.toAPIType_def) lemma createObject_cte_wp_at': "\\s. Types_H.getObjectSize ty us < word_bits \ is_aligned ptr (Types_H.getObjectSize ty us) \ pspace_no_overlap' ptr (Types_H.getObjectSize ty us) s \ cte_wp_at' (\c. P c) slot s \ pspace_aligned' s \ pspace_distinct' s\ RetypeDecls_H.createObject ty ptr us d \\r s. cte_wp_at' (\c. P c) slot s \" apply (simp add:createObject_def) apply (rule hoare_pre) apply (wpc | wp createObjects_orig_cte_wp_at'[where sz = "(Types_H.getObjectSize ty us)"] threadSet_cte_wp_at' | simp add: ARM_H.createObject_def placeNewDataObject_def unless_def placeNewObject_def2 objBitsKO_simps range_cover_full curDomain_def pageBits_def ptBits_def pdBits_def getObjSize_simps archObjSize_def apiGetObjectSize_def tcbBlockSizeBits_def epSizeBits_def ntfnSizeBits_def cteSizeBits_def | intro conjI impI | clarsimp dest!: arch_toAPIType_simps)+ done lemma createObject_getCTE_commute: "monad_commute (cte_wp_at' (\_. True) dests and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (Types_H.getObjectSize ty us) and K (ptr \ dests) and K (Types_H.getObjectSize ty us < word_bits) and K (is_aligned ptr (Types_H.getObjectSize ty us))) (RetypeDecls_H.createObject ty ptr us d) (getCTE dests)" apply (rule monad_commute_guard_imp[OF commute_commute]) apply (rule getCTE_commute) apply (rule hoare_pre) apply (wp createObject_cte_wp_at') apply (clarsimp simp:cte_wp_at_ctes_of) apply assumption apply (clarsimp simp:cte_wp_at_ctes_of) done lemma simpler_placeNewObject_def: "\us < word_bits;is_aligned ptr (objBitsKO (injectKOS val) + us); pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s \ \ placeNewObject ptr val us s = modify (ksPSpace_update (\_. foldr (\addr map. map(addr \ injectKOS val)) (new_cap_addrs (2 ^ us) ptr (injectKOS val)) (ksPSpace s))) s" apply (clarsimp simp:placeNewObject_def2) apply (clarsimp simp:createObjects'_def) apply (simp add:bind_def in_monad when_def is_aligned_mask[THEN iffD1]) apply (clarsimp simp:return_def bind_def gets_def assert_def fail_def get_def split_def split:option.splits) apply (clarsimp simp: new_cap_addrs_fold' word_1_le_power[where 'a=32, folded word_bits_def] lookupAround2_char1 not_less) apply (drule(1) pspace_no_overlapD'[rotated]) apply (drule_tac x = a in in_empty_interE) apply clarsimp apply (drule(1) pspace_alignedD') apply (simp add:is_aligned_no_overflow) apply (clarsimp simp: is_aligned_neg_mask_eq shiftL_nat p_assoc_help) apply simp done lemma fail_set: "fst (fail s) = {}" by (clarsimp simp: fail_def) lemma locateCTE_cte_no_fail: "no_fail (cte_at' src) (locateCTE src)" apply (clarsimp simp:no_fail_def cte_wp_at'_def getObject_def locateCTE_def return_def gets_def get_def bind_def split_def assert_opt_def assert_def in_fail fail_set split:option.splits) apply (clarsimp simp:cte_check_def ObjectInstances_H.loadObject_cte) apply (drule in_singleton) by (auto simp: objBits_simps cteSizeBits_def alignError_def alignCheck_def in_monad is_aligned_mask magnitudeCheck_def typeError_def cong: if_cong split: if_splits option.splits kernel_object.splits) lemma not_in_new_cap_addrs: "\is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; ksPSpace s dest = Some ko;pspace_aligned' s\ \ dest \ set (new_cap_addrs (2 ^ us) ptr obj)" apply (rule ccontr) apply simp apply (drule(1) pspace_no_overlapD'[rotated]) apply (erule_tac x = dest in in_empty_interE) apply (clarsimp) apply (erule(1) is_aligned_no_overflow[OF pspace_alignedD']) apply (erule subsetD[rotated]) apply (simp add:p_assoc_help) apply (rule new_cap_addrs_subset[unfolded ptr_add_def,simplified]) apply (rule range_cover_rel[OF range_cover_full]) apply simp+ done lemma placeNewObject_pspace_aligned': "\K (is_aligned ptr (objBitsKO (injectKOS val) + us) \ objBitsKO (injectKOS val) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)\ placeNewObject ptr val us \\r s. pspace_aligned' s\" apply (clarsimp simp:valid_def) apply (simp add:simpler_placeNewObject_def simpler_modify_def) apply (subst data_map_insert_def[symmetric])+ apply (erule(2) Retype_R.retype_aligned_distinct' [unfolded data_map_insert_def[symmetric]]) apply (rule range_cover_rel[OF range_cover_full]) apply simp+ done lemma placeNewObject_pspace_distinct': "\\s. objBitsKO (injectKOS val) + us < word_bits \ is_aligned ptr (objBitsKO (injectKOS val) + us) \ pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \ pspace_aligned' s \ pspace_distinct' s\ placeNewObject ptr val us \\a. pspace_distinct'\" apply (clarsimp simp:valid_def) apply (simp add:simpler_placeNewObject_def simpler_modify_def) apply (subst data_map_insert_def[symmetric])+ apply (erule(2) Retype_R.retype_aligned_distinct' [unfolded data_map_insert_def[symmetric]]) apply (rule range_cover_rel[OF range_cover_full]) apply simp+ done lemma placeNewObject_ko_wp_at': "\\s. (if slot \ set (new_cap_addrs (2 ^ us) ptr (injectKOS val)) then P (injectKOS val) else ko_wp_at' P slot s) \ objBitsKO (injectKOS val) + us < word_bits \ is_aligned ptr (objBitsKO (injectKOS val) + us) \ pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \ pspace_aligned' s \ pspace_distinct' s\ placeNewObject ptr val us \\a. ko_wp_at' P slot\" apply (clarsimp simp:valid_def split del:if_split) apply (simp add:simpler_placeNewObject_def simpler_modify_def) apply (subst data_map_insert_def[symmetric])+ apply (subst retype_ko_wp_at') apply simp+ apply (rule range_cover_rel[OF range_cover_full]) apply simp+ done lemma cte_wp_at_cases_mask': "cte_wp_at' P p = (\s. (obj_at' P p s \ p && mask 9 \ dom tcb_cte_cases \ obj_at' (P \ fst (the (tcb_cte_cases (p && mask 9)))) (p && ~~ mask 9) s))" apply (rule ext) apply (simp add:cte_wp_at_obj_cases_mask) done lemma not_in_new_cap_addrs': "\dest \ set (new_cap_addrs (2 ^ us) ptr obj); is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; pspace_aligned' s \ \ ksPSpace s dest = None" apply (rule ccontr) apply clarsimp apply (drule not_in_new_cap_addrs) apply simp+ done lemma placeNewObject_cte_wp_at': "\K (is_aligned ptr (objBitsKO (injectKOS val) + us) \ objBitsKO (injectKOS val) + us < word_bits) and K (ptr \ src) and cte_wp_at' P src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)\ placeNewObject ptr val us \\r s. cte_wp_at' P src s\" apply (clarsimp simp:placeNewObject_def2) apply (wp createObjects_orig_cte_wp_at') apply (auto simp:range_cover_full) done lemma placeNewObject_cte_wp_at'': "\\s. cte_wp_at' P slot s \ objBitsKO (injectKOS val) + us < word_bits \ is_aligned ptr (objBitsKO (injectKOS val) + us) \ pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \ pspace_aligned' s \ pspace_distinct' s\ placeNewObject ptr val us \\a s. cte_wp_at' P slot s\" apply (simp add:cte_wp_at_cases_mask' obj_at'_real_def) apply (wp hoare_vcg_disj_lift) apply (wp placeNewObject_ko_wp_at') apply (clarsimp simp:conj_comms) apply (intro conjI impI allI impI) apply (drule(4) not_in_new_cap_addrs') apply (clarsimp simp:ko_wp_at'_def) apply (drule (4)not_in_new_cap_addrs')+ apply (clarsimp simp:ko_wp_at'_def) apply (elim disjE) apply simp apply clarsimp apply (drule (4)not_in_new_cap_addrs')+ apply (clarsimp simp:ko_wp_at'_def) done lemma no_fail_placeNewObject: "no_fail (\s. us < word_bits \ is_aligned ptr (objBitsKO (injectKOS val) + us) \ pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \ pspace_aligned' s) (placeNewObject ptr val us)" by (clarsimp simp:no_fail_def simpler_modify_def simpler_placeNewObject_def) lemma placeNewObject_locateCTE_commute: "monad_commute (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \ (objBitsKO (injectKOS val) + us) < word_bits \ ptr \ src) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and pspace_aligned' and pspace_distinct' and cte_at' src) (placeNewObject ptr val us) (locateCTE src)" apply (rule monad_commute_guard_imp) apply (rule commute_commute[OF locateCTE_commute]) apply (wp no_fail_placeNewObject locateCTE_cte_no_fail placeNewObject_pspace_aligned' placeNewObject_pspace_distinct' placeNewObject_ko_wp_at' | simp)+ apply (clarsimp simp:ko_wp_at'_def) apply (drule(3) not_in_new_cap_addrs) apply fastforce+ apply (wp placeNewObject_cte_wp_at'') apply clarsimp apply fastforce done lemma update_ksPSpaceI: "kh = kh' \ s\ksPSpace := kh\ = s\ksPSpace := kh'\" by simp lemma placeNewObject_modify_commute: "monad_commute (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \ objBitsKO (injectKOS val) + us < word_bits) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and pspace_aligned' and ko_wp_at' (\a. objBitsKO (f (Some a)) = objBitsKO a) ptr') (placeNewObject ptr val us) (modify (ksPSpace_update (\ps. ps(ptr' \ f (ps ptr')))))" apply (clarsimp simp:monad_commute_def simpler_modify_def bind_def split_def return_def) apply (subst simpler_placeNewObject_def) apply ((simp add:range_cover_def)+)[4] apply (clarsimp simp: simpler_modify_def) apply (frule(1) range_cover_full) apply (simp add: simpler_placeNewObject_def) apply (subgoal_tac "pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) (ksPSpace_update (\ps. ps(ptr' \ f (ps ptr'))) s)") prefer 2 apply (clarsimp simp:ko_wp_at'_def) apply (subst pspace_no_overlap'_def) apply (intro allI impI) apply (case_tac "x = ptr'") apply (subgoal_tac "objBitsKO koa = objBitsKO ko") apply (drule(1) pspace_no_overlapD') apply (clarsimp simp:field_simps) apply (clarsimp) apply (drule_tac x = x and s = s in pspace_no_overlapD'[rotated]) apply (simp) apply (clarsimp simp:field_simps) apply (subgoal_tac "pspace_aligned' (ksPSpace_update (\ps. ps(ptr' \ f (ps ptr'))) s)") prefer 2 apply (subst pspace_aligned'_def) apply (rule ballI) apply (erule domE) apply (clarsimp simp:ko_wp_at'_def split:if_split_asm) apply (drule(1) pspace_alignedD')+ apply simp apply (simp add:simpler_placeNewObject_def) apply (clarsimp simp:simpler_modify_def Fun.comp_def singleton_iff image_def) apply (intro conjI update_ksPSpaceI ext) apply (clarsimp simp:ko_wp_at'_def foldr_upd_app_if) apply (frule(1) pspace_no_overlapD') apply (drule subsetD[rotated]) apply (rule new_cap_addrs_subset) apply (erule range_cover_rel) apply simp apply simp apply (drule_tac x = ptr' in in_empty_interE) apply (clarsimp simp:is_aligned_no_overflow) apply (clarsimp simp:range_cover_def ptr_add_def is_aligned_neg_mask_eq obj_range'_def p_assoc_help) apply simp done lemma cte_update_objBits[simp]: "(objBitsKO (cte_update cte b src a)) = objBitsKO b" by (case_tac b, (simp add:objBitsKO_simps cte_update_def)+) lemma locateCTE_ret_neq: "\ko_wp_at' (\x. koTypeOf x \ TCBT \ koTypeOf x \ CTET) ptr\ locateCTE src \\r s. ptr \ r\" apply (clarsimp simp add:valid_def) apply (frule use_valid[OF _ locateCTE_case]) apply simp apply (frule(1) use_valid[OF _ locateCTE_inv]) apply (clarsimp simp:ko_wp_at'_def koTypeOf_def) apply (auto split:Structures_H.kernel_object.split_asm) done lemma locateCTE_ko_wp_at': "\cte_at' src and pspace_distinct' \ locateCTE src \\rv. ko_wp_at' \ rv \" apply (clarsimp simp:locateCTE_def split_def) apply wp apply (clarsimp simp:cte_wp_at'_def getObject_def gets_def split_def get_def bind_def return_def ko_wp_at'_def lookupAround2_char1 assert_opt_def) apply (clarsimp split:option.splits simp:fail_def return_def lookupAround2_char1) apply (case_tac ba) apply (simp_all add:cte_check_def) apply (clarsimp simp:lookupAround2_char1 objBits_simps cte_update_def) apply (drule(1) pspace_distinctD')+ apply (simp add:objBits_simps) apply (clarsimp simp:objBits_simps cte_update_def) apply (drule(1) pspace_distinctD')+ apply (simp add:objBits_simps) done lemma setCTE_placeNewObject_commute: "monad_commute (K (is_aligned ptr (objBitsKO (injectKOS val) + us) \ objBitsKO (injectKOS val) + us < word_bits) and K(ptr \ src) and cte_wp_at' (\_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us)) (setCTE src cte) (placeNewObject ptr val us)" apply (clarsimp simp: setCTE_def2 split_def) apply (rule commute_commute) apply (rule monad_commute_guard_imp) apply (rule monad_commute_split[OF placeNewObject_modify_commute]) apply (rule placeNewObject_locateCTE_commute) apply (wp locateCTE_inv locateCTE_ko_wp_at' | simp)+ done lemma getCTE_doMachineOp_commute: "monad_commute (cte_wp_at' (\_. True) dest) (getCTE dest) (doMachineOp x)" apply (rule monad_commute_guard_imp) apply (rule getCTE_commute) apply wp apply fastforce+ done lemma doMachineOp_upd_heap_commute: "monad_commute \ (doMachineOp x) (modify (ksPSpace_update P))" apply (clarsimp simp:doMachineOp_def split_def simpler_modify_def gets_def get_def return_def bind_def select_f_def) apply (clarsimp simp:monad_commute_def bind_def return_def) apply fastforce done lemma magnitudeCheck_det: "\ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); ps_clear ptr (objBitsKO ko) s\ \ magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s = ({((), s)},False)" apply (frule in_magnitude_check'[THEN iffD2]) apply (case_tac ko) apply (simp add:objBitsKO_simps pageBits_def)+ apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object) apply (simp add:archObjSize_def pageBits_def)+ apply (subgoal_tac "\ snd (magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s)") apply (drule singleton_in_magnitude_check) apply (drule_tac x = s in spec) apply (case_tac "(magnitudeCheck ptr (snd (lookupAround2 ptr (ksPSpace s))) (objBitsKO ko) s)") apply simp apply (rule ccontr) apply (clarsimp simp:magnitudeCheck_assert assert_def fail_def return_def split:if_splits option.splits) done lemma getPDE_det: "ko_wp_at' (op = (KOArch (KOPDE pde))) p s \ getObject p s = ({((pde::ARM_H.pde),s)},False)" apply (clarsimp simp:ko_wp_at'_def getObject_def split_def bind_def gets_def return_def get_def assert_opt_def split:if_splits) apply (clarsimp simp: fail_def return_def lookupAround2_known1) apply (simp add: loadObject_default_def) apply (clarsimp simp:projectKO_def projectKO_opt_pde alignCheck_def is_aligned_mask objBits_simps unless_def) apply (clarsimp simp:bind_def return_def) apply (intro conjI) apply (intro set_eqI iffI) apply clarsimp apply (subst (asm) in_magnitude_check') apply (simp add:archObjSize_def is_aligned_mask)+ apply (rule bexI[rotated]) apply (rule in_magnitude_check'[THEN iffD2]) apply (simp add:is_aligned_mask)+ apply (clarsimp simp:image_def) apply (clarsimp simp:magnitudeCheck_assert assert_def objBits_def archObjSize_def return_def fail_def lookupAround2_char2 split:option.splits if_split_asm) apply (rule ccontr) apply (simp add:ps_clear_def field_simps) apply (erule_tac x = x2 in in_empty_interE) apply (clarsimp simp:less_imp_le) apply (rule conjI) apply (subst add.commute) apply (rule word_diff_ls') apply (clarsimp simp:field_simps not_le plus_one_helper) apply (simp add:field_simps is_aligned_no_wrap' is_aligned_mask) apply simp apply auto done lemma pde_at_obj_at': "ko_wp_at' (op = (KOArch (KOPDE (pde::pde)))) ptr s = obj_at' (op = pde) ptr s" by(clarsimp simp:obj_at'_real_def ko_wp_at'_def projectKO_PDE) lemma in_dom_eq: "m a = Some obj \ dom (\b. if b = a then Some g else m b) = dom m" by (rule set_eqI,clarsimp simp:dom_def) lemma setCTE_pde_at': "\ko_wp_at' (op = (KOArch (KOPDE pde))) ptr and cte_wp_at' (\_. True) src and pspace_distinct'\ setCTE src cte \\x s. ko_wp_at' (op = (KOArch (KOPDE pde))) ptr s\" apply (clarsimp simp:setCTE_def2) apply wp apply (simp add:split_def) apply (clarsimp simp:valid_def) apply (subgoal_tac "b = s") prefer 2 apply (erule use_valid[OF _ locateCTE_inv]) apply simp apply (subgoal_tac "ptr \ a") apply (frule use_valid[OF _ locateCTE_ko_wp_at']) apply simp apply (clarsimp simp:ko_wp_at'_def ps_clear_def) apply (simp add:in_dom_eq) apply (drule use_valid[OF _ locateCTE_case]) apply simp apply (clarsimp simp:ko_wp_at'_def objBits_simps archObjSize_def) done lemma getPDE_setCTE_commute: "monad_commute (pde_at' ptr and pspace_distinct' and cte_wp_at' (\_. True) src) (setCTE src cte) (getObject ptr :: KernelStateData_H.kernel_state \ (pde \ KernelStateData_H.kernel_state) set \ bool)" apply (rule commute_name_pre_state) apply (clarsimp simp:typ_at'_def ko_wp_at'_def) apply (case_tac ko,simp_all) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all) apply clarsimp apply (rename_tac pde) apply (subgoal_tac "ko_wp_at' (op = (KOArch (KOPDE pde))) ptr s") prefer 2 apply (clarsimp simp:ko_wp_at'_def) apply (rule monad_commute_guard_imp) apply (rule commute_commute) apply (rule commute_rewrite[OF getPDE_det,where R = \]) apply assumption apply (wp setCTE_pde_at') apply (simp add:monad_commute_def bind_def) apply (auto simp:ko_wp_at'_def) done lemma getPDE_doMachineOp_commute: "monad_commute (pde_at' ptr) (doMachineOp f) ((getObject ptr) :: KernelStateData_H.kernel_state \ (pde \ KernelStateData_H.kernel_state) set \ bool)" apply (rule commute_name_pre_state) apply (clarsimp simp:typ_at'_def ko_wp_at'_def) apply (case_tac ko,simp_all) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all) apply clarsimp apply (rename_tac pde) apply (subgoal_tac "ko_wp_at' (op = (KOArch (KOPDE pde))) ptr s") prefer 2 apply (clarsimp simp:ko_wp_at'_def) apply (rule monad_commute_guard_imp) apply (rule commute_commute) apply (rule commute_rewrite[OF getPDE_det,where R = \]) apply assumption apply (wp setCTE_pde_at') apply (simp add:monad_commute_def bind_def) apply auto done lemma getPDE_placeNewObject_commute: "monad_commute (pde_at' src and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) and K (is_aligned ptr (objBitsKO (injectKOS val) + sz) \ objBitsKO (injectKOS val) + sz < word_bits) ) (placeNewObject ptr val sz) ((getObject src) :: KernelStateData_H.kernel_state \ (pde \ KernelStateData_H.kernel_state) set \ bool)" apply (rule commute_name_pre_state) apply (subgoal_tac "range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)") prefer 2 apply (rule range_cover_full) apply simp+ apply (clarsimp simp:typ_at'_def ko_wp_at'_def) apply (case_tac ko,simp_all) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all) apply clarsimp apply (rename_tac pde) apply (subgoal_tac "ko_wp_at' (op = (KOArch (KOPDE pde))) src s") prefer 2 apply (clarsimp simp:ko_wp_at'_def) apply (rule monad_commute_guard_imp) apply (rule commute_commute) apply (rule commute_rewrite[OF getPDE_det,where R = \]) apply assumption apply (simp add:placeNewObject_def2) apply (wp createObjects_orig_ko_wp_at2') apply (simp add:monad_commute_def bind_def) apply (auto simp:ko_wp_at'_def) done lemma storePDE_det: "ko_wp_at' (op = (KOArch (KOPDE pde))) ptr s \ storePDE ptr (new_pde::ARM_H.pde) s = modify (ksPSpace_update (\_. ksPSpace s(ptr \ KOArch (KOPDE new_pde)))) s" apply (clarsimp simp:ko_wp_at'_def storePDE_def split_def bind_def gets_def return_def get_def setObject_def assert_opt_def split:if_splits) apply (clarsimp simp:lookupAround2_known1 return_def alignCheck_def updateObject_default_def split_def archObjSize_def unless_def projectKO_def projectKO_opt_pde bind_def when_def is_aligned_mask[symmetric] objBits_simps) apply (drule magnitudeCheck_det) apply (simp add:objBits_simps archObjSize_def)+ apply (simp add:simpler_modify_def) done lemma modify_obj_commute: "monad_commute (K (ptr\ ptr')) (modify (ksPSpace_update (\ps. ps(ptr \ ko)))) (modify (ksPSpace_update (\ps. ps(ptr' \ ko'))))" apply (clarsimp simp:monad_commute_def return_def bind_def simpler_modify_def) apply (case_tac s) apply auto done lemma modify_specify: "(\s. modify (ksPSpace_update (\_. P (ksPSpace s))) s) = modify (ksPSpace_update (\ps. P ps))" by (auto simp: simpler_modify_def) lemma modify_specify2: "(modify (ksPSpace_update (\_. P (ksPSpace s))) >>= g) s = (modify (ksPSpace_update (\ps. P ps)) >>=g) s" apply (clarsimp simp:simpler_modify_def bind_def) apply (rule arg_cong[where f = "\x. g () x"],simp) done lemma modify_pde_pde_at': "\pde_at' ptr\ modify (ksPSpace_update (\ps. ps(ptr \ KOArch (KOPDE new_pde)))) \\a. pde_at' ptr\" apply wp apply (clarsimp simp del: fun_upd_apply simp: typ_at'_def ko_wp_at'_def objBits_simps archObjSize_def) apply (clarsimp simp:ps_clear_def) apply (case_tac ko,simp_all) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all) apply (clarsimp simp:archObjSize_def) done lemma modify_pde_pspace_distinct': "\pde_at' ptr and pspace_distinct'\ modify (ksPSpace_update (\ps. ps(ptr \ KOArch (KOPDE new_pde)))) \\a. pspace_distinct'\" apply (clarsimp simp: simpler_modify_def ko_wp_at'_def valid_def typ_at'_def) apply (case_tac ko; simp) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all) apply (subst pspace_distinct'_def) apply (intro ballI) apply (erule domE) apply (clarsimp split:if_splits) apply (drule(1) pspace_distinctD') apply (simp add:objBits_simps archObjSize_def) apply (simp add:ps_clear_def) apply (drule_tac x = x in pspace_distinctD') apply simp unfolding ps_clear_def apply (erule disjoint_subset2[rotated]) apply clarsimp done lemma modify_pde_pspace_aligned': "\pde_at' ptr and pspace_aligned'\ modify (ksPSpace_update (\ps. ps(ptr \ KOArch (KOPDE new_pde)))) \\a. pspace_aligned'\" apply (clarsimp simp: simpler_modify_def ko_wp_at'_def valid_def typ_at'_def) apply (case_tac ko,simp_all) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all) apply (subst pspace_aligned'_def) apply (intro ballI) apply (erule domE) apply (clarsimp split:if_splits) apply (drule(1) pspace_alignedD') apply (simp add:objBits_simps archObjSize_def) apply (simp add:ps_clear_def) apply (drule_tac x = x in pspace_alignedD') apply simp apply simp done lemma modify_pde_psp_no_overlap': "\pde_at' ptr and pspace_no_overlap' ptr' sz\ modify (ksPSpace_update (\ps. ps(ptr \ KOArch (KOPDE new_pde)))) \\a. pspace_no_overlap' ptr' sz\" proof - note 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 show ?thesis apply (clarsimp simp:simpler_modify_def ko_wp_at'_def valid_def typ_at'_def) apply (case_tac ko,simp_all) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all) apply (subst pspace_no_overlap'_def) apply (intro allI impI) apply (clarsimp split:if_splits) apply (drule(1) pspace_no_overlapD') apply (simp add:objBits_simps archObjSize_def field_simps) apply (drule(1) pspace_no_overlapD')+ apply (simp add:field_simps) done qed lemma koTypeOf_pde: "koTypeOf ko = ArchT PDET \ \pde. ko = KOArch (KOPDE pde)" apply (case_tac ko,simp_all) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all) done lemma modify_mapM_x: "(modify (ksPSpace_update (foldr (\addr map. map(addr \ obj)) list))) = (mapM_x (\x. modify (ksPSpace_update (\m. m(x\ obj)))) (rev list))" apply (induct list) apply (clarsimp simp:mapM_x_Nil) apply (rule ext) apply (simp add:simpler_modify_def return_def) apply (clarsimp simp:mapM_x_append mapM_x_singleton simpler_modify_def) apply (drule sym) apply (rule ext) apply (simp add:Fun.comp_def bind_def) done lemma doMachineOp_storePDE_commute: "monad_commute (pde_at' src) (doMachineOp f) (storePDE src (new_pde::ARM_H.pde))" proof - have eq_fail: "\sa ks. snd (doMachineOp f (sa\ksPSpace := ks\)) = snd (doMachineOp f sa)" apply (clarsimp simp:doMachineOp_def bind_def return_def gets_def get_def simpler_modify_def select_def) apply (intro iffI) apply (elim disjE) apply (clarsimp simp:image_def select_f_def)+ done show ?thesis apply (rule commute_name_pre_state) apply (clarsimp simp:typ_at'_def ko_wp_at'_def) apply (case_tac ko,simp_all) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all) apply clarsimp apply (rename_tac pde) apply (subgoal_tac "ko_wp_at' (op = (KOArch (KOPDE pde))) src s") prefer 2 apply (clarsimp simp:ko_wp_at'_def) apply (rule monad_commute_guard_imp) apply (rule commute_commute) apply (rule commute_rewrite[OF storePDE_det,where R = "\"]) apply assumption apply wp apply (clarsimp simp:monad_commute_def simpler_modify_def return_def bind_def) apply (intro conjI iffI set_eqI) apply (clarsimp simp:doMachineOp_def gets_def bind_def get_def select_f_def return_def) apply (erule bexI[rotated]) apply (clarsimp simp:simpler_modify_def) apply (clarsimp simp:doMachineOp_def gets_def bind_def get_def select_f_def return_def) apply (erule bexI[rotated]) apply (clarsimp simp:simpler_modify_def) apply (simp add:eq_fail image_def) apply (elim disjE) apply clarsimp apply (clarsimp simp:doMachineOp_def gets_def bind_def get_def select_f_def return_def) apply (clarsimp simp:eq_fail) apply auto done qed lemma storePDE_placeNewObject_commute: "monad_commute (pde_at' src and pspace_distinct' and pspace_aligned' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) and K (is_aligned ptr (objBitsKO (injectKOS val) + sz) \ objBitsKO (injectKOS val) + sz < word_bits) ) (placeNewObject ptr val sz) (storePDE src (new_pde::ARM_H.pde))" apply (rule commute_name_pre_state) apply (clarsimp simp:typ_at'_def ko_wp_at'_def) apply (case_tac ko,simp_all) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all) apply clarsimp apply (rename_tac pde) apply (subgoal_tac "ko_wp_at' (op = (KOArch (KOPDE pde))) src s") prefer 2 apply (clarsimp simp:ko_wp_at'_def) apply (subgoal_tac "range_cover ptr (objBitsKO (injectKOS val) + sz) (objBitsKO (injectKOS val) + sz) (Suc 0)") prefer 2 apply (rule range_cover_full) apply simp+ apply (rule monad_commute_guard_imp) apply (rule commute_commute) apply (rule commute_rewrite[OF storePDE_det]) apply assumption apply (simp add:placeNewObject_def2) apply (wp createObjects_orig_ko_wp_at2') apply (rule commute_commute) apply (subst modify_specify2[where g = "return",simplified]) apply (rule_tac commute_rewrite[where Q = "\s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + sz) s \ pde_at' src s \ pspace_distinct' s \ pspace_aligned' s"]) apply (rule simpler_placeNewObject_def) apply simp+ apply (wp modify_pde_psp_no_overlap' modify_pde_pspace_distinct' modify_pde_pspace_aligned' modify_pde_pde_at') apply (simp add: modify_specify modify_mapM_x) apply (rule commute_commute[OF mapM_x_commute[where f = id]]) apply (rule modify_obj_commute) apply wp apply simp apply clarsimp apply (intro conjI,simp_all) apply (clarsimp simp:typ_at'_def ko_wp_at'_def objBits_simps archObjSize_def) apply (rule new_cap_addrs_distinct) apply (erule range_cover_rel) apply simp+ apply clarsimp apply (simp add:not_in_new_cap_addrs) done lemma modify_obj_commute': "monad_commute (K (ptr\ ptr') and ko_wp_at' \ ptr') (modify (ksPSpace_update (\ps. ps(ptr \ ko)))) (modify (ksPSpace_update (\ps. ps(ptr' \ f (the (ps ptr'))))))" apply (clarsimp simp:monad_commute_def return_def bind_def simpler_modify_def ko_wp_at'_def) apply (case_tac s) apply clarsimp apply (rule ext) apply clarsimp done lemma cte_wp_at_modify_pde: notes blah[simp del] = atLeastatMost_subset_iff atLeastLessThan_iff Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex atLeastAtMost_iff shows "\ksPSpace s ptr' = Some (KOArch (KOPDE pde)); pspace_aligned' s;cte_wp_at' \ ptr s\ \ cte_wp_at' \ ptr (s\ksPSpace := ksPSpace s(ptr' \ (KOArch (KOPDE pde')))\)" apply (simp add:cte_wp_at_obj_cases_mask obj_at'_real_def) apply (frule(1) pspace_alignedD') apply (elim disjE) apply (rule disjI1) apply (clarsimp simp add:ko_wp_at'_def) apply (intro conjI impI) apply (simp add:objBitsKO_simps archObjSize_def) apply (clarsimp simp:projectKO_opt_cte) apply (simp add:ps_clear_def)+ apply (clarsimp simp:objBitsKO_simps archObjSize_def) apply (simp add:ps_clear_def) apply (rule ccontr) apply simp apply (erule in_emptyE, blast) apply simp apply (rule disjI2) apply (clarsimp simp:ko_wp_at'_def) apply (intro conjI impI) apply (simp add:objBitsKO_simps archObjSize_def)+ apply (clarsimp simp:projectKO_opt_cte projectKO_opt_tcb) apply (simp add:ps_clear_def)+ apply (clarsimp simp:objBitsKO_simps archObjSize_def) apply (simp add:ps_clear_def) apply (rule ccontr) apply simp apply (erule in_emptyE) apply blast done lemma storePDE_setCTE_commute: notes blah[simp del] = atLeastatMost_subset_iff atLeastLessThan_iff Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex atLeastAtMost_iff shows "monad_commute (pde_at' ptr and pspace_distinct' and pspace_aligned' and cte_wp_at' (\_. True) src) (setCTE src cte) (storePDE ptr (new_pde::ARM_H.pde))" apply (rule commute_name_pre_state) apply (clarsimp simp:typ_at'_def ko_wp_at'_def) apply (case_tac ko,simp_all) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all) apply clarsimp apply (rename_tac pde) apply (subgoal_tac "ko_wp_at' (op = (KOArch (KOPDE pde))) ptr s") prefer 2 apply (clarsimp simp:ko_wp_at'_def) apply (rule monad_commute_guard_imp) apply (rule commute_commute) apply (rule commute_rewrite[OF storePDE_det]) apply assumption apply (wp setCTE_pde_at') apply (simp add:setCTE_def2) apply (rule monad_commute_split) apply (subst modify_specify) apply (rule modify_obj_commute') apply (rule commute_commute[OF locateCTE_commute]) apply (wp locateCTE_cte_no_fail non_fail_modify modify_pde_pspace_distinct' modify_pde_pspace_aligned'| subst modify_specify)+ apply (clarsimp simp:simpler_modify_def valid_def typ_at'_def) apply (clarsimp simp:ko_wp_at'_def dest!: koTypeOf_pde) apply (intro conjI impI) apply (clarsimp simp:objBitsKO_simps archObjSize_def)+ apply (simp add:ps_clear_def in_dom_eq) apply (simp add:ps_clear_def in_dom_eq) apply (clarsimp simp:simpler_modify_def valid_def) apply (clarsimp simp:typ_at'_def ko_wp_at'_def) apply (case_tac ko,simp_all add:koTypeOf_def )[1] apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object,simp_all add:archTypeOf_def)[1] apply (erule(2) cte_wp_at_modify_pde) apply wp apply (thin_tac "cte_wp_at' P src s" for P s)+ apply (clarsimp simp: typ_at'_def cte_wp_at_obj_cases_mask obj_at'_real_def) apply (wp locateCTE_ret_neq locateCTE_ko_wp_at') apply (clarsimp simp:ko_wp_at'_def objBits_simps archObjSize_def typ_at'_def) apply fastforce done lemma setCTE_gets_globalPD_commute: "monad_commute (cte_wp_at' (\_. True) src and pspace_distinct' and pspace_aligned') (setCTE src cte) (gets (armKSGlobalPD \ ksArchState))" apply (simp add:setCTE_def2) apply (rule monad_commute_guard_imp) apply (rule commute_commute[OF monad_commute_split[where Q = "\r. \"]]) apply (clarsimp simp:monad_commute_def gets_def simpler_modify_def bind_def get_def return_def) apply (rule commute_commute[OF locateCTE_commute]) apply (wp locateCTE_cte_no_fail) apply clarsimp apply (wp|clarsimp)+ apply fastforce done lemma placeNewObject_gets_globalPD_commute: "monad_commute (pspace_distinct' and pspace_aligned' and K (us < word_bits \ is_aligned ptr (objBitsKO (injectKOS val) + us)) and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) ) (placeNewObject ptr val us) (gets (armKSGlobalPD \ ksArchState))" apply (rule commute_name_pre_state) apply (rule monad_commute_guard_imp) apply (rule_tac commute_rewrite[where Q = "\s. pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s \ pspace_distinct' s \ pspace_aligned' s" and R = "\"]) apply (rule simpler_placeNewObject_def) apply simp+ apply wp apply (simp add:monad_commute_def gets_def get_def return_def bind_def simpler_modify_def) apply clarsimp done (* FIXME: move *) lemmas of_nat_inj32 = of_nat_inj[where 'a=32, folded word_bits_def] lemma copyGlobalMappings_setCTE_commute: "monad_commute (valid_arch_state' and pspace_distinct' and pspace_aligned' and cte_wp_at' (\_. True) src and page_directory_at' ptr) (copyGlobalMappings ptr) (setCTE src cte)" apply (clarsimp simp:copyGlobalMappings_def) apply (rule monad_commute_guard_imp) apply (rule commute_commute[OF monad_commute_split]) apply (rule mapM_x_commute[where f = id]) apply (rule monad_commute_split[OF _ getPDE_setCTE_commute]) apply (rule storePDE_setCTE_commute) apply wp apply clarsimp apply (rule setCTE_gets_globalPD_commute) apply wp apply (clarsimp simp:valid_arch_state'_def page_directory_at'_def objBits_simps archObjSize_def pdBits_def pageBits_def) apply (drule le_m1_iff_lt[where x = "(0x1000::word32)",simplified,THEN iffD1]) apply clarsimp done lemma setCTE_doMachineOp_commute: assumes nf: "no_fail Q (doMachineOp x)" shows "monad_commute (cte_at' dest and pspace_aligned' and pspace_distinct' and Q) (setCTE dest cte) (doMachineOp x)" apply (simp add:setCTE_def2 split_def) apply (rule monad_commute_guard_imp) apply (rule commute_commute[OF monad_commute_split]) apply (rule doMachineOp_upd_heap_commute) apply (rule commute_commute[OF locateCTE_commute]) apply (wp nf locateCTE_cte_no_fail) apply clarsimp apply (wp|clarsimp|fastforce)+ done lemma setCTE_unless_doMachineOp_commute: assumes nf: "no_fail Q (doMachineOp x)" shows "monad_commute (cte_at' dest and pspace_aligned' and pspace_distinct' and Q) (setCTE dest cte) (unless d (doMachineOp x))" apply (simp add: unless_def when_def) apply safe apply (wp nf setCTE_doMachineOp_commute) apply (rule commute_commute) apply (rule monad_commute_guard_imp) apply (rule return_commute) apply simp done lemma placeNewObject_valid_arch_state: "\valid_arch_state' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and pspace_aligned' and pspace_distinct' and K (is_aligned ptr (objBitsKO (injectKOS val) + us)) and K ( (objBitsKO (injectKOS val)+ us)< word_bits)\ placeNewObject ptr val us \\rv s. valid_arch_state' s\" apply (simp add:placeNewObject_def2 split_def) apply (rule createObjects'_wp_subst) apply (wp createObjects_valid_arch) apply clarsimp apply (intro conjI,simp) apply (erule(1) range_cover_full) done lemma placeNewObject_pd_at': "\K (is_aligned ptr pdBits) and pspace_no_overlap' ptr pdBits and pspace_aligned' and pspace_distinct'\ placeNewObject ptr (makeObject::ARM_H.pde) (pdBits - objBits (makeObject::ARM_H.pde)) \\rv s. page_directory_at' ptr s\" apply (simp add:page_directory_at'_def typ_at'_def) apply (rule hoare_pre) apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift placeNewObject_ko_wp_at') apply (clarsimp simp:objBits_simps archObjSize_def) apply (intro conjI) apply (clarsimp simp:pdBits_def pageBits_def word_bits_def)+ apply (clarsimp simp:pdBits_def pageBits_def new_cap_addrs_def objBits_simps archObjSize_def image_def) apply (drule_tac x = "unat x" in bspec) apply clarsimp apply (rule unat_less_helper) apply simp apply simp done lemma setCTE_modify_gsCNode_commute: "monad_commute P (setCTE src (cte::cte)) (modify (%ks. ks\gsCNodes := f (gsCNodes ks)\))" by (auto simp: monad_commute_def setCTE_def setObject_def split_def bind_def return_def simpler_modify_def simpler_gets_def assert_opt_def fail_def simpler_updateObject_def split: option.splits if_split_asm) lemma setCTE_modify_gsUserPages_commute: "monad_commute P (setCTE src (cte::cte)) (modify (%ks. ks\gsUserPages := f (gsUserPages ks)\))" by (auto simp: monad_commute_def setCTE_def setObject_def split_def bind_def return_def simpler_modify_def simpler_gets_def assert_opt_def fail_def simpler_updateObject_def split: option.splits if_split_asm) lemma getTCB_det: "ko_wp_at' (op = (KOTCB tcb)) p s \ getObject p s = ({(tcb,s)},False)" apply (clarsimp simp:ko_wp_at'_def getObject_def split_def bind_def gets_def return_def get_def assert_opt_def split:if_splits) apply (clarsimp simp: fail_def return_def lookupAround2_known1) apply (simp add:loadObject_default_def) apply (clarsimp simp:projectKO_def projectKO_opt_tcb alignCheck_def is_aligned_mask objBits_simps unless_def) apply (clarsimp simp:bind_def return_def) apply (intro conjI) apply (intro set_eqI iffI) apply clarsimp apply (subst (asm) in_magnitude_check') apply (simp add:archObjSize_def is_aligned_mask)+ apply (rule bexI[rotated]) apply (rule in_magnitude_check'[THEN iffD2]) apply (simp add:is_aligned_mask)+ apply (clarsimp simp:image_def) apply (clarsimp simp:magnitudeCheck_assert assert_def objBits_def archObjSize_def return_def fail_def lookupAround2_char2 split:option.splits if_split_asm) apply (rule ccontr) apply (simp add:ps_clear_def field_simps) apply (erule_tac x = x2 in in_empty_interE) apply (clarsimp simp:less_imp_le) apply (rule conjI) apply (subst add.commute) apply (rule word_diff_ls') apply (clarsimp simp:field_simps not_le plus_one_helper) apply (simp add:field_simps is_aligned_no_wrap' is_aligned_mask) apply simp apply auto done lemma threadSet_det: "tcb_at' ptr s \ threadSet f ptr s = modify (ksPSpace_update (\ps. ps(ptr \ (\t. case t of Some (KOTCB tcb) \ KOTCB (f tcb)) (ps ptr)))) s" apply (clarsimp simp add:threadSet_def bind_def obj_at'_def) apply (clarsimp simp:projectKO_eq projectKO_opt_tcb split: Structures_H.kernel_object.splits) apply (subst getTCB_det,simp add:ko_wp_at'_def)+ apply (clarsimp simp:setObject_def gets_def get_def) apply (subst bind_def) apply (clarsimp simp:split_def) apply (simp add:lookupAround2_known1 bind_assoc projectKO_def assert_opt_def updateObject_default_def projectKO_opt_tcb) apply (clarsimp simp add: alignCheck_def unless_def when_def is_aligned_mask objBits_simps) apply (clarsimp simp:magnitudeCheck_det bind_def) apply (cut_tac ko = "KOTCB obj" in magnitudeCheck_det) apply (simp add:objBits_simps is_aligned_mask)+ apply (clarsimp simp:modify_def get_def put_def bind_def) done lemma setCTE_modify_tcbDomain_commute: " monad_commute (tcb_at' ptr and cte_wp_at' (\_. True) src and pspace_distinct' and pspace_aligned') (setCTE src cte) (threadSet (tcbDomain_update (\_. ra)) ptr)" proof - note blah[simp del] = atLeastatMost_subset_iff atLeastLessThan_iff Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex atLeastAtMost_iff have hint: "\P ptr a cte b src ra. monad_commute (tcb_at' ptr and ko_wp_at' P a ) (threadSet (tcbDomain_update (\_. ra)) ptr) (modify (ksPSpace_update (\ps. ps(a \ cte_update cte (the (ps a)) src a))))" apply (clarsimp simp add: monad_commute_def bind_def simpler_modify_def return_def) apply (clarsimp simp:threadSet_det simpler_modify_def) apply (subgoal_tac "tcb_at' ptr (ksPSpace_update (\ps. ps(a \ cte_update cte (the (ps a)) src a)) s)") prefer 2 apply (clarsimp simp:obj_at'_def) apply (intro conjI impI) apply simp apply (clarsimp simp:projectKO_eq projectKO_opt_tcb split:Structures_H.kernel_object.split_asm) apply (simp add:cte_update_def) apply (clarsimp simp:projectKO_eq projectKO_opt_tcb split:Structures_H.kernel_object.split_asm) apply (simp add:ps_clear_def) apply (clarsimp simp:projectKO_eq projectKO_opt_tcb split:Structures_H.kernel_object.split_asm) apply (simp add:ps_clear_def) apply (rule ccontr,simp) apply (erule in_emptyE) apply (clarsimp simp:ko_wp_at'_def) apply blast apply (simp add:threadSet_det simpler_modify_def) apply (subst (asm) obj_at'_def) apply (thin_tac "tcb_at' ptr P" for P) apply (clarsimp simp: obj_at'_def projectKO_eq projectKO_opt_tcb, simp split: Structures_H.kernel_object.split_asm) apply (case_tac s,clarsimp) apply (intro conjI) apply clarsimp apply (rule ext,clarsimp) apply (case_tac obj) apply (simp add:cte_update_def) apply clarsimp apply (rule ext) apply simp done show ?thesis apply (rule commute_name_pre_state) apply (clarsimp simp add: setCTE_def2) apply (rule monad_commute_guard_imp) apply (rule commute_commute[OF monad_commute_split]) apply (rule hint) apply (rule commute_commute) apply (rule locateCTE_commute) apply (wp locateCTE_cte_no_fail) apply (wp threadSet_ko_wp_at2') apply (clarsimp simp:objBitsKO_simps) apply (wp|simp)+ apply (wp locateCTE_inv locateCTE_ko_wp_at') apply clarsimp apply fastforce done qed lemma curDomain_commute: assumes cur:"\P. \\s. P (ksCurDomain s)\ f \\r s. P (ksCurDomain s)\" shows "monad_commute \ f curDomain" apply (clarsimp simp add:monad_commute_def curDomain_def get_def return_def gets_def bind_def) apply (rule conjI) apply (rule set_eqI) apply (rule iffI) apply clarsimp apply (rule bexI[rotated], assumption) apply clarsimp apply (frule_tac P1 = "\x. x = ksCurDomain s" in use_valid[OF _ cur]) apply simp+ apply clarsimp apply (rule bexI[rotated], assumption) apply clarsimp apply (frule_tac P1 = "\x. x = ksCurDomain s" in use_valid[OF _ cur]) apply simp+ apply auto done crunch inv[wp]: curDomain P lemma placeNewObject_tcb_at': notes blah[simp del] = atLeastatMost_subset_iff atLeastLessThan_iff Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex atLeastAtMost_iff shows "\pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBits (makeObject::tcb)) and K(is_aligned ptr (objBits (makeObject::tcb))) \ placeNewObject ptr (makeObject::tcb) 0 \\rv s. tcb_at' ptr s \" apply (simp add:placeNewObject_def placeNewObject'_def split_def) apply (wp hoare_unless_wp |wpc | simp add:alignError_def)+ apply (auto simp:obj_at'_def is_aligned_mask lookupAround2_None1 lookupAround2_char1 field_simps is_aligned_neg_mask_eq projectKO_opt_tcb projectKO_def return_def ps_clear_def split:if_splits dest!:pspace_no_overlap_disjoint' )[1] apply (drule_tac m = "ksPSpace s" in domI) apply (erule in_emptyE) apply (fastforce simp:objBits_simps) done (* Some times the weak if version of monad_commute is enough *) lemma monad_commute_if_weak_l: "\monad_commute P1 f1 h; monad_commute P2 f2 h\ \ monad_commute (P1 and P2) (if d then f1 else f2) h" apply (clarsimp) apply (intro conjI impI) apply (erule monad_commute_guard_imp,simp)+ done lemma monad_commute_if_weak_r: "\monad_commute P1 f h1; monad_commute P2 f h2\ \ monad_commute (P1 and P2) f (if d then h1 else h2)" apply (clarsimp) apply (intro conjI impI) apply (erule monad_commute_guard_imp,simp)+ done lemma createObject_setCTE_commute: "monad_commute (cte_wp_at' (\_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (Types_H.getObjectSize ty us) and valid_arch_state' and K (ptr \ src) and K (is_aligned ptr (Types_H.getObjectSize ty us)) and K (Types_H.getObjectSize ty us < word_bits)) (RetypeDecls_H.createObject ty ptr us d) (setCTE src cte)" apply (rule commute_grab_asm)+ apply (subgoal_tac "ptr && mask (Types_H.getObjectSize ty us) = 0") prefer 2 apply (clarsimp simp: range_cover_def is_aligned_mask) apply (clarsimp simp: createObject_def) apply (case_tac ty, simp_all add: ARM_H.toAPIType_def) apply (rename_tac apiobject_type) apply (case_tac apiobject_type) apply (simp_all add: ARM_H.getObjectSize_def apiGetObjectSize_def tcbBlockSizeBits_def epSizeBits_def ntfnSizeBits_def cteSizeBits_def) -- Untyped apply (simp add: monad_commute_guard_imp[OF return_commute]) -- "TCB, EP, NTFN" apply (rule monad_commute_guard_imp[OF commute_commute]) apply (rule monad_commute_split[OF monad_commute_split]) apply (rule monad_commute_split[OF commute_commute[OF return_commute]]) apply (rule setCTE_modify_tcbDomain_commute) apply wp apply (rule curDomain_commute) apply wp apply (rule setCTE_placeNewObject_commute) apply (wp placeNewObject_tcb_at' placeNewObject_cte_wp_at' placeNewObject_pspace_distinct' placeNewObject_pspace_aligned' | clarsimp simp:objBitsKO_simps)+ apply (rule monad_commute_guard_imp[OF commute_commute] ,rule monad_commute_split[OF commute_commute[OF return_commute]] ,rule setCTE_placeNewObject_commute ,(wp|clarsimp simp:objBitsKO_simps)+)+ -- CNode apply (rule monad_commute_guard_imp[OF commute_commute]) apply (rule monad_commute_split)+ apply (rule return_commute[THEN commute_commute]) apply (rule setCTE_modify_gsCNode_commute[of \]) apply (rule hoare_triv[of \]) apply wp apply (rule setCTE_placeNewObject_commute) apply (wp|clarsimp simp:objBitsKO_simps)+ -- "Arch Objects" apply ((rule monad_commute_guard_imp[OF commute_commute] , rule monad_commute_split[OF commute_commute[OF return_commute]] , clarsimp simp: ARM_H.createObject_def placeNewDataObject_def bind_assoc split del: if_splits ,(rule monad_commute_split return_commute[THEN commute_commute] setCTE_modify_gsUserPages_commute[of \] modify_wp[of "%_. \"] setCTE_unless_doMachineOp_commute setCTE_doMachineOp_commute setCTE_placeNewObject_commute monad_commute_if_weak_r copyGlobalMappings_setCTE_commute[THEN commute_commute] | wp placeNewObject_pspace_distinct' placeNewObject_pspace_aligned' placeNewObject_cte_wp_at' placeNewObject_valid_arch_state placeNewObject_pd_at' | erule is_aligned_weaken | simp add: objBits_simps pageBits_def ptBits_def pdBits_def archObjSize_def split del: if_splits)+)+) done lemma createObject_updateMDB_commute: "monad_commute ((\s. src \ 0 \ cte_wp_at' (\_. True) src s) and pspace_no_overlap' ptr (Types_H.getObjectSize ty us) and pspace_aligned' and pspace_distinct' and valid_arch_state' and K (ptr \ src) and K (is_aligned ptr (Types_H.getObjectSize ty us)) and K ((Types_H.getObjectSize ty us)< word_bits)) (updateMDB src f) (RetypeDecls_H.createObject ty ptr us d)" apply (clarsimp simp:updateMDB_def split:if_split_asm) apply (intro conjI impI) apply (simp add: monad_commute_guard_imp[OF return_commute]) apply (rule monad_commute_guard_imp) apply (rule commute_commute[OF monad_commute_split]) apply (rule createObject_setCTE_commute) apply (rule createObject_getCTE_commute) apply wp apply (auto simp:range_cover_full) done lemma updateMDB_pspace_no_overlap': "\pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz\ updateMDB slot f \\rv s. pspace_no_overlap' ptr sz s\" apply (rule hoare_pre) apply (clarsimp simp: updateMDB_def split del: if_split) apply (wp setCTE_pspace_no_overlap') apply clarsimp done lemma ctes_of_ko_at: "ctes_of s p = Some a \ (\ptr ko. (ksPSpace s ptr = Some ko \ p \ obj_range' ptr ko))" apply (clarsimp simp: map_to_ctes_def Let_def split: if_split_asm) apply (intro exI conjI, assumption) apply (simp add: obj_range'_def objBits_simps is_aligned_no_wrap' field_simps) apply (intro exI conjI, assumption) apply (clarsimp simp: objBits_simps obj_range'_def word_and_le2) apply (thin_tac "P" for P)+ apply (simp add: mask_def) apply word_bitwise done lemma pspace_no_overlapD2': "\is_aligned ptr sz; pspace_no_overlap' ptr sz s;sz < word_bits; ctes_of s slot = Some cte\ \ slot \ ptr" apply (drule ctes_of_ko_at) apply clarsimp apply (drule(1) pspace_no_overlapD') apply (erule in_empty_interE) apply (simp add:obj_range'_def) apply clarsimp apply (subst is_aligned_neg_mask_eq[symmetric]) apply simp apply (rule is_aligned_no_overflow) apply (simp add:is_aligned_neg_mask) done lemma caps_overlap_reserved'_subseteq: "\caps_overlap_reserved' B s; A\ B\ \ caps_overlap_reserved' A s" apply (clarsimp simp:caps_overlap_reserved'_def) apply (drule(1) bspec) apply (erule disjoint_subset2) apply simp done definition weak_valid_dlist where "weak_valid_dlist \ \m. (\p cte. m p = Some cte \ (let next = mdbNext (cteMDBNode cte) in (next \ 0 \ (\cte'. m next = Some cte' \ cteCap cte'\ capability.NullCap))))" lemma valid_arch_state'_updateMDB: "\valid_arch_state' \ updateMDB a b \\rv. valid_arch_state'\" by (clarsimp simp:updateMDB_def valid_arch_state_def,wp) lemma fail_commute: "monad_commute \ fail f = empty_fail f" apply (simp add: monad_commute_def empty_fail_def) apply (simp add: fail_def bind_def del: split_paired_Ex) apply blast done lemma modify_commute: "monad_commute P (modify f) (modify g) = (\s. P s \ f (g s) = g (f s))" apply (simp add: monad_commute_def exec_modify) apply (simp add: return_def eq_commute) done lemma createObjects_gsUntypedZeroRanges_commute': "monad_commute \ (createObjects' ptr n ko us) (modify (\s. s \ gsUntypedZeroRanges := f (gsUntypedZeroRanges s) \ ))" apply (simp add: createObjects'_def unless_def when_def alignError_def fail_commute) apply clarsimp apply (rule commute_commute) apply (strengthen monad_commute_guard_imp[OF monad_commute_split[where P="\" and Q="\\"], OF _ _ hoare_vcg_prop] | simp add: modify_commute split: option.split prod.split)+ apply (simp add: monad_commute_def exec_modify exec_gets assert_def) done lemma assert_commute2: "empty_fail f \ monad_commute \ (assert G) f" apply (clarsimp simp:assert_def monad_commute_def) apply (simp add: fail_def bind_def empty_fail_def del: split_paired_Ex) apply blast done lemma threadSet_gsUntypedZeroRanges_commute': "monad_commute \ (threadSet fn ptr) (modify (\s. s \ gsUntypedZeroRanges := f (gsUntypedZeroRanges s) \ ))" apply (simp add: threadSet_def getObject_def setObject_def) apply (rule commute_commute) apply (strengthen monad_commute_guard_imp[OF monad_commute_split[where P="\" and Q="\\"], OF _ _ hoare_vcg_prop] | simp add: modify_commute updateObject_default_def alignCheck_assert magnitudeCheck_assert return_commute return_commute[THEN commute_commute] projectKO_def2 assert_commute2 assert_commute2[THEN commute_commute] assert_opt_def2 loadObject_default_def split: option.split prod.split)+ apply (simp add: monad_commute_def exec_gets exec_modify) done lemma doMachineOp_modify_commute: "\ \s. P s \ ksMachineState (f s) = ksMachineState s; \s. P s \ (\(rv, ms') \ fst (oper (ksMachineState s)). f (ksMachineState_update (\_. ms') s) = ksMachineState_update (\_. ms') (f s)) \ \ monad_commute P (doMachineOp oper) (modify (f))" apply (clarsimp simp: monad_commute_def doMachineOp_def exec_gets bind_assoc exec_modify) apply (simp add: bind_def[where f="select_f v" for v], simp add: select_f_def split_def exec_modify cart_singleton_image) done lemma copyGlobalMappings_gsUntypedZeroRanges_commute': "monad_commute \ (copyGlobalMappings ptr) (modify (\s. s \ gsUntypedZeroRanges := f (gsUntypedZeroRanges s) \ ))" apply (simp add: copyGlobalMappings_def) apply (rule monad_commute_guard_imp) apply (rule commute_commute[OF monad_commute_split[where P="\"]]) apply (rule mapM_x_commute[where f = id and P="\\"]) apply (simp add: storePDE_def getObject_def setObject_def cong: bind_cong) apply (strengthen monad_commute_guard_imp[OF monad_commute_split[where P="\" and Q="\\"], OF _ _ hoare_vcg_prop] | simp add: modify_commute updateObject_default_def alignCheck_assert magnitudeCheck_assert return_commute return_commute[THEN commute_commute] projectKO_def2 assert_commute2 assert_commute2[THEN commute_commute] assert_opt_def2 loadObject_default_def split: option.split prod.split)+ apply (simp add: monad_commute_def exec_gets exec_modify) apply wp apply (simp add: monad_commute_def exec_gets exec_modify) apply wp apply simp done lemma createObject_gsUntypedZeroRanges_commute: "monad_commute \ (RetypeDecls_H.createObject ty ptr us dev) (modify (\s. s \ gsUntypedZeroRanges := f (gsUntypedZeroRanges s) \ ))" apply (simp add: createObject_def ARM_H.createObject_def placeNewDataObject_def placeNewObject_def2 bind_assoc fail_commute return_commute toAPIType_def split: option.split apiobject_type.split object_type.split) apply (strengthen monad_commute_guard_imp[OF monad_commute_split[where P="\" and Q="\\"], OF _ _ hoare_vcg_prop, THEN commute_commute] monad_commute_guard_imp[OF monad_commute_split[where P="\" and Q="\\"], OF _ _ hoare_vcg_prop] | simp add: modify_commute createObjects_gsUntypedZeroRanges_commute' createObjects_gsUntypedZeroRanges_commute'[THEN commute_commute] return_commute return_commute[THEN commute_commute] threadSet_gsUntypedZeroRanges_commute'[THEN commute_commute] doMachineOp_modify_commute[THEN commute_commute] copyGlobalMappings_gsUntypedZeroRanges_commute'[THEN commute_commute] split: option.split prod.split cong: if_cong)+ apply (simp add: curDomain_def monad_commute_def exec_modify exec_gets) done lemma monad_commute_If_rhs: "monad_commute P a b \ monad_commute Q a c \ monad_commute (\s. (R \ P s) \ (\ R \ Q s)) a (if R then b else c)" by simp lemma case_eq_if_isUntypedCap: "(case c of UntypedCap _ _ _ _ \ x | _ \ y) = (if isUntypedCap c then x else y)" by (cases c, simp_all add: isCap_simps) lemma createObject_updateTrackedFreeIndex_commute: "monad_commute (cte_wp_at' (\_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (Types_H.getObjectSize ty us) and valid_arch_state' and K (ptr \ slot) and K (Types_H.getObjectSize ty us < word_bits) and K (is_aligned ptr (Types_H.getObjectSize ty us))) (RetypeDecls_H.createObject ty ptr us dev) (updateTrackedFreeIndex slot idx)" apply (simp add: updateTrackedFreeIndex_def getSlotCap_def updateCap_def) apply (rule monad_commute_guard_imp) apply (rule monad_commute_split[OF _ createObject_getCTE_commute] monad_commute_split[OF _ createObject_gsUntypedZeroRanges_commute] createObject_gsUntypedZeroRanges_commute)+ apply (wp getCTE_wp') apply (clarsimp simp: pspace_no_overlap'_def) done lemma createObject_updateNewFreeIndex_commute: "monad_commute (cte_wp_at' (\_. True) slot and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (Types_H.getObjectSize ty us) and valid_arch_state' and K (ptr \ slot) and K (Types_H.getObjectSize ty us < word_bits) and K (is_aligned ptr (Types_H.getObjectSize ty us))) (RetypeDecls_H.createObject ty ptr us dev) (updateNewFreeIndex slot)" apply (simp add: updateNewFreeIndex_def getSlotCap_def case_eq_if_isUntypedCap updateTrackedFreeIndex_def) apply (rule monad_commute_guard_imp) apply (rule monad_commute_split[OF _ createObject_getCTE_commute]) apply (rule monad_commute_If_rhs) apply (rule createObject_updateTrackedFreeIndex_commute) apply (rule commute_commute[OF return_commute]) apply (wp getCTE_wp') apply clarsimp done lemma new_cap_object_comm_helper: "monad_commute (pspace_aligned' and pspace_distinct' and (\s. no_0 (ctes_of s)) and (\s. weak_valid_dlist (ctes_of s)) and (\s. valid_nullcaps (ctes_of s)) and cte_wp_at' (\c. isUntypedCap (cteCap c)) parent and cte_wp_at' (\c. cteCap c = capability.NullCap) slot and pspace_no_overlap' ptr (Types_H.getObjectSize ty us) and valid_arch_state' and K (Types_H.getObjectSize ty us capability.NullCap) and K (is_aligned ptr (Types_H.getObjectSize ty us) \ ptr \ 0 \ parent \ 0)) (RetypeDecls_H.createObject ty ptr us d) (insertNewCap parent slot cap)" apply (clarsimp simp:insertNewCap_def bind_assoc liftM_def) apply (rule monad_commute_guard_imp) apply (rule monad_commute_split[OF _ createObject_getCTE_commute])+ apply (rule monad_commute_split[OF _ commute_commute[OF assert_commute]]) apply (rule monad_commute_split[OF _ createObject_setCTE_commute]) apply (rule monad_commute_split[OF _ commute_commute[OF createObject_updateMDB_commute]]) apply (rule monad_commute_split[OF _ commute_commute[OF createObject_updateMDB_commute]]) apply (rule createObject_updateNewFreeIndex_commute) apply (wp getCTE_wp hoare_vcg_imp_lift hoare_vcg_disj_lift valid_arch_state'_updateMDB updateMDB_pspace_no_overlap' setCTE_pspace_no_overlap' | clarsimp simp:conj_comms)+ apply (clarsimp simp:cte_wp_at_ctes_of) apply (frule_tac slot = slot in pspace_no_overlapD2') apply simp+ apply (frule_tac slot = parent in pspace_no_overlapD2') apply simp+ apply (case_tac ctea,clarsimp) apply (frule_tac p = slot in nullcapsD') apply simp+ apply (subgoal_tac "(mdbNext (cteMDBNode cte) = 0 \ (\ctea. ctes_of s (mdbNext (cteMDBNode cte)) = Some ctea))") apply (elim disjE) apply clarsimp+ apply (frule_tac slot = "(mdbNext (cteMDBNode cte))" in pspace_no_overlapD2') apply simp+ apply (clarsimp simp:weak_valid_dlist_def) apply (drule_tac x = "parent " in spec) apply clarsimp done lemma pspace_no_overlap_gsUntypedZeroRanges[simp]: "pspace_no_overlap' ptr n (gsUntypedZeroRanges_update f s) = pspace_no_overlap' ptr n s" by (simp add: pspace_no_overlap'_def) crunch pspace_aligned'[wp]: updateNewFreeIndex "pspace_aligned'" crunch pspace_distinct'[wp]: updateNewFreeIndex "pspace_distinct'" crunch valid_arch_state'[wp]: updateNewFreeIndex "valid_arch_state'" crunch pspace_no_overlap'[wp]: updateNewFreeIndex "pspace_no_overlap' ptr n" crunch ctes_of[wp]: updateNewFreeIndex "\s. P (ctes_of s)" lemma updateNewFreeIndex_cte_wp_at[wp]: "\\s. P (cte_wp_at' P' p s)\ updateNewFreeIndex slot \\rv s. P (cte_wp_at' P' p s)\" by (simp add: cte_wp_at_ctes_of, wp) lemma new_cap_object_commute: "monad_commute (cte_wp_at' (\c. isUntypedCap (cteCap c)) parent and (\s. \slot\set list. cte_wp_at' (\c. cteCap c = capability.NullCap) slot s) and pspace_no_overlap' ptr (Types_H.getObjectSize ty us) and valid_pspace' and valid_arch_state' and K (distinct (map fst (zip list caps))) and K (\cap \ set caps. cap \ capability.NullCap) and K (Types_H.getObjectSize ty us ptr \ 0)) (RetypeDecls_H.createObject ty ptr us d) (zipWithM_x (insertNewCap parent) list caps)" apply (clarsimp simp:zipWithM_x_mapM_x) apply (rule monad_commute_guard_imp) apply (rule mapM_x_commute[where f = fst]) apply (simp add:split_def) apply (rule new_cap_object_comm_helper) apply (clarsimp simp:insertNewCap_def split_def) apply (wp updateMDB_weak_cte_wp_at updateMDB_pspace_no_overlap' getCTE_wp valid_arch_state'_updateMDB setCTE_weak_cte_wp_at setCTE_pspace_no_overlap') apply (clarsimp simp:cte_wp_at_ctes_of simp del:fun_upd_apply) apply (case_tac "parent \ aa") prefer 2 apply simp apply (clarsimp simp: conj_comms) apply (intro conjI exI) apply (clarsimp simp: no_0_def) apply (clarsimp simp: weak_valid_dlist_def modify_map_def Let_def) subgoal by (intro conjI impI; fastforce) apply (clarsimp simp:valid_nullcaps_def) apply (frule_tac x = "p" in spec) apply (case_tac ctec) apply (case_tac cte) apply (rename_tac cap' node') apply (case_tac node') apply (rename_tac word1 word2 bool1 bool2) apply (clarsimp simp:modify_map_def split:if_split_asm) apply (case_tac z) apply (drule_tac x = word1 in spec) apply (clarsimp simp:weak_valid_dlist_def) apply (drule_tac x = parent in spec) apply clarsimp apply (clarsimp simp:valid_pspace'_def valid_mdb'_def valid_mdb_ctes_def) apply (intro conjI) apply (clarsimp simp:weak_valid_dlist_def Let_def) apply (frule(2) valid_dlist_nextD) apply clarsimp apply (case_tac cte') apply clarsimp apply (drule_tac m = "ctes_of s" in nullcapsD') apply simp apply (clarsimp simp: no_0_def nullPointer_def) apply (erule in_set_zipE) apply clarsimp apply (erule in_set_zipE) apply clarsimp apply (clarsimp simp:cte_wp_at_ctes_of) done lemma createObjects'_pspace_no_overlap: "gz = (objBitsKO val) + us \ \pspace_no_overlap' (ptr + (1 + of_nat n << gz)) gz and K (range_cover ptr sz gz (Suc (Suc n)) \ ptr \ 0)\ createObjects' ptr (Suc n) val us \\addrs s. pspace_no_overlap' (ptr + (1 + of_nat n << gz)) gz s\" proof - note simps [simp del] = untyped_range.simps usable_untyped_range.simps atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex assume "gz = (objBitsKO val) + us" thus ?thesis apply - apply (rule hoare_gen_asm) apply (clarsimp simp:createObjects'_def split_def new_cap_addrs_fold') apply (subst new_cap_addrs_fold') apply clarsimp apply (drule range_cover_le[where n = "Suc n"]) apply simp apply (drule_tac gbits = us in range_cover_not_zero_shift[rotated]) apply simp+ apply (simp add:word_le_sub1) apply (wp haskell_assert_wp hoare_unless_wp | wpc |simp add:alignError_def del:fun_upd_apply)+ apply (rule conjI) apply (rule impI) apply (subgoal_tac "pspace_no_overlap' (ptr + (1 + of_nat n << objBitsKO val + us)) (objBitsKO val + us) (s\ksPSpace := foldr (\addr map. map(addr \ val)) (new_cap_addrs (unat (1 + of_nat n << us)) ptr val) (ksPSpace s)\)") apply (intro conjI impI allI) apply assumption+ apply (subst pspace_no_overlap'_def) apply (intro allI impI) apply (subst (asm) foldr_upd_app_if) apply (subst is_aligned_neg_mask_eq) apply (rule aligned_add_aligned[OF range_cover.aligned],assumption) apply (rule is_aligned_shiftl_self) apply (simp add:range_cover_def) apply simp apply (clarsimp split:if_splits) apply (drule obj_range'_subset_strong[rotated]) apply (rule range_cover_rel[OF range_cover_le[where n = "Suc n"]],assumption) apply simp apply simp apply (drule range_cover.unat_of_nat_n_shift [OF range_cover_le[where n = "Suc n"],where gbits = us]) apply simp apply (simp add:shiftl_t2n field_simps)+ apply (simp add:obj_range'_def) apply (erule disjoint_subset) apply (clarsimp simp: simps) apply (thin_tac "x \ y" for x y) apply (subst (asm) le_m1_iff_lt[THEN iffD1]) apply (drule_tac range_cover_no_0[rotated,where p = "Suc n"]) apply simp apply simp apply (simp add:field_simps) apply (simp add: power_add[symmetric]) apply (simp add: word_neq_0_conv) apply (simp add: power_add[symmetric] field_simps) apply (frule range_cover_subset[where p = "Suc n"]) apply simp apply simp apply (drule(1) pspace_no_overlapD') apply (subst (asm) is_aligned_neg_mask_eq) apply (rule aligned_add_aligned[OF range_cover.aligned],assumption) apply (rule is_aligned_shiftl_self) apply (simp add:range_cover_def) apply simp apply (simp add:word_le_sub1 shiftl_t2n field_simps) apply auto done qed lemma createNewCaps_not_nc: "\\\ createNewCaps ty ptr (Suc (length as)) us d \\r s. (\cap\set r. cap \ capability.NullCap)\" apply (clarsimp simp:simp:createNewCaps_def Arch_createNewCaps_def ) apply (rule hoare_pre) apply wpc apply wp apply (simp add:Arch_createNewCaps_def split del: if_split) apply (wpc|wp|clarsimp)+ done lemma doMachineOp_psp_no_overlap: "\\s. pspace_no_overlap' ptr sz s \ pspace_aligned' s \ pspace_distinct' s \ doMachineOp f \\y s. pspace_no_overlap' ptr sz s\" by (wp pspace_no_overlap'_lift,simp) lemma unless_doMachineOp_psp_no_overlap: "\\s. pspace_no_overlap' ptr sz s \ pspace_aligned' s \ pspace_distinct' s \ unless d $ doMachineOp f \\y s. pspace_no_overlap' ptr sz s\" by (wp hoare_unless_wp doMachineOp_psp_no_overlap, simp) lemma createObjects'_psp_distinct: "\pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and K (range_cover ptr sz ((objBitsKO ko) + us) n \ n \ 0 \ is_aligned ptr (objBitsKO ko + us) \ objBitsKO ko + us < word_bits)\ createObjects' ptr n ko us \\rv s. pspace_distinct' s\" apply (rule hoare_name_pre_state) apply (clarsimp simp:createObjects'_def split_def) apply (subst new_cap_addrs_fold') apply (drule range_cover_not_zero_shift[where gbits = us,rotated]) apply simp+ apply unat_arith apply (rule hoare_pre) apply (wpc|wp|simp add: unless_def alignError_def del: fun_upd_apply)+ apply clarsimp apply (subst data_map_insert_def[symmetric])+ apply (simp add: range_cover.unat_of_nat_n_shift) apply (drule(2) retype_aligned_distinct'(1)[where ko = ko and n= "n*2^us" ]) apply (erule range_cover_rel) apply simp apply clarsimp apply (simp add: range_cover.unat_of_nat_n_shift) done lemma createObjects'_psp_aligned: "\pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and K (range_cover ptr sz ((objBitsKO ko) + us) n \ n \ 0 \ is_aligned ptr (objBitsKO ko + us) \ objBitsKO ko + us < word_bits)\ createObjects' ptr n ko us \\rv s. pspace_aligned' s\" apply (rule hoare_name_pre_state) apply (clarsimp simp: createObjects'_def split_def) apply (subst new_cap_addrs_fold') apply (drule range_cover_not_zero_shift[where gbits = us,rotated]) apply simp+ apply unat_arith apply (rule hoare_pre) apply (wpc|wp|simp add: unless_def alignError_def del: fun_upd_apply)+ apply clarsimp apply (frule(2) retype_aligned_distinct'(2)[where ko = ko and n= "n*2^us" ]) apply (erule range_cover_rel) apply simp apply clarsimp apply (subst data_map_insert_def[symmetric])+ apply (simp add: range_cover.unat_of_nat_n_shift) done lemma copyGlobalMappings_pspace_no_overlap': "\pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz\ copyGlobalMappings xa \\ya. pspace_no_overlap' ptr sz\" apply (rule hoare_pre) apply (clarsimp simp:copyGlobalMappings_def) apply (wp mapM_x_wp_inv pspace_no_overlap'_lift) apply clarsimp done lemma pspace_no_overlap'_le: assumes psp: "pspace_no_overlap' ptr sz s" "sz'\ sz" assumes b: "sz < word_bits" shows "pspace_no_overlap' ptr sz' s" proof - note 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 have diff_cancel: "\a b c. (a::word32) + b - c = b + (a - c)" by simp have bound :"(ptr && ~~ mask sz') - (ptr && ~~ mask sz) \ 2 ^ sz - 2 ^ sz'" by (rule neg_mask_diff_bound[OF psp(2)]) show ?thesis using psp apply (clarsimp simp:pspace_no_overlap'_def) apply (drule_tac x = x in spec) apply clarsimp apply (erule disjoint_subset2[rotated]) apply (clarsimp simp:blah) apply (rule word_plus_mcs[OF _ is_aligned_no_overflow']) apply (simp add:diff_cancel p_assoc_help) apply (rule le_plus) apply (simp add:field_simps) apply (rule bound) apply (rule word_le_minus_mono_left) apply (erule two_power_increasing[OF _ b[unfolded word_bits_def]]) apply (rule word_1_le_power) using b[unfolded word_bits_def] apply simp apply (simp add:is_aligned_neg_mask) done qed lemma pspace_no_overlap'_le2: assumes "pspace_no_overlap' ptr sz s" "ptr \ ptr'" "ptr' &&~~ mask sz = ptr && ~~ mask sz" shows "pspace_no_overlap' ptr' sz s" proof - note 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 show ?thesis using assms apply (clarsimp simp:pspace_no_overlap'_def) apply (drule_tac x = x in spec) apply clarsimp apply (erule disjoint_subset2[rotated]) apply (clarsimp simp:blah) done qed lemma pspace_no_overlap'_tail: "\range_cover ptr sz us (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \ 0\ \ pspace_no_overlap' (ptr + (1 + of_nat n << us)) sz s" apply (erule pspace_no_overlap'_le2) apply (erule(1) range_cover_ptr_le) apply (erule(1) range_cover_tail_mask) done lemma createNewCaps_pspace_no_overlap': "\\s. range_cover ptr sz (Types_H.getObjectSize ty us) (Suc (Suc n)) \ pspace_aligned' s \ pspace_distinct' s \ pspace_no_overlap' ptr sz s \ ptr \ 0\ createNewCaps ty ptr (Suc n) us d \\r s. pspace_no_overlap' (ptr + (1 + of_nat n << Types_H.getObjectSize ty us)) (Types_H.getObjectSize ty us) s\" apply (rule hoare_name_pre_state) apply (clarsimp simp: createNewCaps_def) apply (subgoal_tac "pspace_no_overlap' (ptr + (1 + of_nat n << (Types_H.getObjectSize ty us))) (Types_H.getObjectSize ty us) s") prefer 2 apply (rule pspace_no_overlap'_le[where sz = sz]) apply (rule pspace_no_overlap'_tail) apply simp+ apply (simp add:range_cover_def) apply (simp add:range_cover.sz(1)[where 'a=32, folded word_bits_def]) apply (rule_tac Q = "\r. pspace_no_overlap' (ptr + (1 + of_nat n << Types_H.getObjectSize ty us)) (Types_H.getObjectSize ty us) and pspace_aligned' and pspace_distinct'" in hoare_strengthen_post) apply (case_tac ty) apply (simp_all add: apiGetObjectSize_def ARM_H.toAPIType_def tcbBlockSizeBits_def ARM_H.getObjectSize_def objBits_simps epSizeBits_def ntfnSizeBits_def cteSizeBits_def pageBits_def ptBits_def archObjSize_def pdBits_def createObjects_def) apply (rule hoare_pre) apply wpc apply (clarsimp simp: apiGetObjectSize_def curDomain_def ARM_H.toAPIType_def tcbBlockSizeBits_def ARM_H.getObjectSize_def objBits_simps epSizeBits_def ntfnSizeBits_def cteSizeBits_def pageBits_def ptBits_def archObjSize_def pdBits_def createObjects_def Arch_createNewCaps_def split: apiobject_type.splits | wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap[where sz = sz] createObjects'_psp_aligned[where sz = sz] createObjects'_psp_distinct[where sz = sz] copyGlobalMappings_pspace_aligned' mapM_x_wp_inv copyGlobalMappings_pspace_no_overlap'[where sz = sz] | assumption)+ apply (intro conjI range_cover_le[where n = "Suc n"] | simp)+ apply ((simp add:objBits_simps pageBits_def range_cover_def word_bits_def)+)[5] by ((clarsimp simp: apiGetObjectSize_def ARM_H.toAPIType_def tcbBlockSizeBits_def ARM_H.getObjectSize_def objBits_simps epSizeBits_def ntfnSizeBits_def cteSizeBits_def pageBits_def ptBits_def archObjSize_def pdBits_def createObjects_def Arch_createNewCaps_def unless_def split: apiobject_type.splits | wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap createObjects'_psp_aligned createObjects'_psp_distinct copyGlobalMappings_pspace_aligned' mapM_x_wp_inv copyGlobalMappings_pspace_no_overlap' | assumption | clarsimp simp: word_bits_def | intro conjI range_cover_le[where n = "Suc n"] range_cover.aligned)+)[6] lemma objSize_eq_capBits: "Types_H.getObjectSize ty us = APIType_capBits ty us" apply (case_tac ty) apply (clarsimp simp:ARM_H.getObjectSize_def objBits_simps getObjectSize_def APIType_capBits_def apiGetObjectSize_def ptBits_def tcbBlockSizeBits_def epSizeBits_def ntfnSizeBits_def cteSizeBits_def pageBits_def pdBits_def split : apiobject_type.splits)+ done lemma createNewCaps_ret_len: "\K (n < 2 ^ word_bits \ n \ 0)\ createNewCaps ty ptr n us d \\rv s. n = length rv\" apply (rule hoare_name_pre_state) apply clarsimp apply (case_tac ty) apply (simp_all add:createNewCaps_def ARM_H.toAPIType_def ) apply (rule hoare_pre) apply wpc apply (wp|simp add:Arch_createNewCaps_def ARM_H.toAPIType_def unat_of_nat_minus_1 [where 'a=32, folded word_bits_def] | erule hoare_strengthen_post[OF createObjects_ret],clarsimp+ | intro conjI impI)+ apply (rule hoare_pre, (wp | simp add: Arch_createNewCaps_def toAPIType_def ARM_H.toAPIType_def unat_of_nat_minus_1 | erule hoare_strengthen_post[OF createObjects_ret],clarsimp+ | intro conjI impI)+)+ done lemma no_overlap_check: "\range_cover ptr sz bits n; pspace_no_overlap' ptr sz s; pspace_aligned' s;n\ 0\ \ case_option (return ()) (case_prod (\x xa. haskell_assert (x < fromPPtr ptr) [])) (fst (lookupAround2 (ptr + of_nat (shiftL n bits - Suc 0)) (ksPSpace s))) s = return () s" apply (clarsimp split:option.splits simp:assert_def lookupAround2_char1 not_less) apply (rule ccontr) apply (frule(1) pspace_no_overlapD') apply (erule_tac x = a in in_empty_interE) apply clarsimp apply (drule(1) pspace_alignedD') apply (erule is_aligned_no_overflow) apply clarsimp apply (erule order_trans) apply (frule range_cover_cell_subset[where x = "of_nat n - 1"]) apply (rule gt0_iff_gem1[THEN iffD1]) apply (simp add:word_gt_0) apply (rule range_cover_not_zero) apply simp apply assumption apply (clarsimp simp:shiftL_nat field_simps) apply (erule impE) apply (frule range_cover_subset_not_empty[rotated,where x = "of_nat n - 1"]) apply (rule gt0_iff_gem1[THEN iffD1]) apply (simp add:word_gt_0) apply (rule range_cover_not_zero) apply simp apply assumption apply (clarsimp simp:field_simps) apply simp done lemma new_caps_addrs_append: "\range_cover ptr sz (objBitsKO va + us) (Suc n)\ \ new_cap_addrs (unat (of_nat n + (1::word32) << us)) ptr val = new_cap_addrs (unat (((of_nat n)::word32) << us)) ptr val @ new_cap_addrs (unat ((2::word32) ^ us)) ((((of_nat n)::word32) << objBitsKO val + us) + ptr) val" apply (subst add.commute) apply (clarsimp simp:new_cap_addrs_def) apply (subst upt_add_eq_append'[where j="unat (((of_nat n)::word32) << us)"]) prefer 3 apply simp apply (subst upt_lhs_sub_map) apply (simp add:Fun.comp_def field_simps) apply (subst unat_sub[symmetric]) apply (simp add:shiftl_t2n) apply (subst mult.commute) apply (subst mult.commute[where a = "2 ^ us"])+ apply (rule word_mult_le_mono1) apply (simp add:word_le_nat_alt) apply (subst of_nat_Suc[symmetric]) apply (frule range_cover.unat_of_nat_n) apply (drule range_cover.unat_of_nat_n[OF range_cover_le[where n = n]]) apply simp apply simp apply (simp add: p2_gt_0) apply (simp add:range_cover_def word_bits_def) apply (subst word_bits_def[symmetric]) apply (subst of_nat_Suc[symmetric]) apply (subst range_cover.unat_of_nat_n) apply simp apply (subst unat_power_lower) apply (simp add:range_cover_def) apply (frule range_cover.range_cover_n_le(2)) apply (subst mult.commute) apply (rule le_less_trans[OF nat_le_power_trans[where m = sz]]) apply (erule le_trans) apply simp apply (simp add:range_cover_def) apply (simp add:range_cover_def[where 'a=32, folded word_bits_def]) apply (clarsimp simp: power_add [symmetric] shiftl_t2n field_simps) apply simp apply (frule range_cover_le[where n = n]) apply simp apply (drule range_cover_rel[where sbit'= "objBitsKO va"]) apply simp+ apply (drule range_cover_rel[where sbit'= "objBitsKO va"]) apply simp+ apply (drule range_cover.unat_of_nat_n)+ apply (simp add:shiftl_t2n) apply (clarsimp simp: power_add[symmetric] shiftl_t2n field_simps ) done lemma modify_comp: "modify (ksPSpace_update (\a. f (g a))) = (do modify (ksPSpace_update (\a. (g a))); modify (ksPSpace_update (\a. f a)) od)" by (clarsimp simp:simpler_modify_def bind_def Fun.comp_def) lemma modify_objs_commute: "monad_commute (K ((set lst1) \ (set lst2) = {})) (modify (ksPSpace_update (foldr (\addr map. map(addr \ val)) lst1))) (modify (ksPSpace_update (foldr (\addr map. map(addr \ val)) lst2)))" apply (clarsimp simp:monad_commute_def simpler_modify_def bind_def return_def) apply (case_tac s,simp) apply (rule ext) apply (clarsimp simp:foldr_upd_app_if) done lemma new_cap_addrs_disjoint: "\range_cover ptr sz (objBitsKO val + us) (Suc (Suc n))\ \ set (new_cap_addrs (2^us) (((1::word32) + of_nat n << objBitsKO val + us) + ptr) val) \ set (new_cap_addrs (unat ((1::word32) + of_nat n << us)) ptr val) = {}" apply (frule range_cover.unat_of_nat_n_shift[where gbits = us,symmetric]) apply simp apply (frule range_cover_rel[where sbit' = "objBitsKO val"]) apply (simp add:field_simps)+ apply (frule new_cap_addrs_distinct) apply (subst (asm) add.commute[where b = 2])+ apply (subst (asm) new_caps_addrs_append[where n = "Suc n",simplified]) apply (simp add:field_simps) apply (clarsimp simp:field_simps Int_ac range_cover_def) done lemma pspace_no_overlap'_modify: "\K (range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)) \ ptr \ 0) and pspace_no_overlap' (((1::word32) + of_nat n << objBitsKO val + us) + ptr) (objBitsKO val + us)\ modify (ksPSpace_update (foldr (\addr map. map(addr \ val)) (new_cap_addrs (unat ((1::word32) + of_nat n << us)) ptr val))) \\r. pspace_no_overlap' (((1::word32) + of_nat n << objBitsKO val + us) + ptr) (objBitsKO val + us)\" proof - note 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 show ?thesis apply (clarsimp simp:simpler_modify_def valid_def pspace_no_overlap'_def) apply (frule(1) range_cover_tail_mask) apply (simp add:field_simps) apply (drule_tac x = x in spec) apply (clarsimp simp:foldr_upd_app_if split:if_splits) apply (frule obj_range'_subset_strong[rotated]) apply (drule range_cover_le[where n = "Suc n"]) apply simp apply (rule range_cover_rel,assumption) apply simp apply clarsimp apply (frule range_cover.unat_of_nat_n_shift[where gbits = us,symmetric]) apply simp+ apply (simp add:field_simps) apply (simp add:obj_range'_def) apply (erule disjoint_subset) apply (frule(1) range_cover_ptr_le) apply (subgoal_tac "\ ptr + (1 + of_nat n << us + objBitsKO val) \ ptr + (1 + of_nat n << us) * 2 ^ objBitsKO val - 1") apply (clarsimp simp:blah field_simps) apply (clarsimp simp: not_le) apply (rule minus_one_helper) apply (clarsimp simp: power_add[symmetric] shiftl_t2n field_simps objSize_eq_capBits ) apply (rule neq_0_no_wrap) apply (clarsimp simp: power_add[symmetric] shiftl_t2n field_simps objSize_eq_capBits ) apply simp done qed lemma placeNewObject_copyGlobalMapping_commute: "monad_commute (valid_arch_state' and pspace_distinct' and pspace_aligned' and page_directory_at' r and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and K (objBitsKO (injectKOS val) + us < word_bits \ is_aligned ptr (objBitsKO (injectKOS val) + us)) ) (placeNewObject ptr val us) (copyGlobalMappings r)" apply (clarsimp simp:copyGlobalMappings_def) apply (rule monad_commute_guard_imp) apply (rule monad_commute_split) apply (rule mapM_x_commute[where f = id]) apply (rule monad_commute_split[OF _ getPDE_placeNewObject_commute]) apply (rule storePDE_placeNewObject_commute) apply wp apply (wp pspace_no_overlap'_lift | clarsimp)+ apply (rule placeNewObject_gets_globalPD_commute) apply wp apply clarsimp apply (clarsimp simp: valid_arch_state'_def page_directory_at'_def objBits_simps archObjSize_def pdBits_def pageBits_def) apply (drule le_m1_iff_lt[where x = "(0x1000::word32)",simplified,THEN iffD1]) apply (clarsimp) done lemma createObjects_Cons: "\range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); pspace_distinct' s;pspace_aligned' s; pspace_no_overlap' ptr sz s;pspace_aligned' s; ptr \ 0\ \ createObjects' ptr (Suc (Suc n)) val us s = (do createObjects' ptr (Suc n) val us; createObjects' (((1 + of_nat n) << (objBitsKO val + us)) + ptr) (Suc 0) val us od) s" apply (clarsimp simp:createObjects'_def split_def bind_assoc) apply (subgoal_tac "is_aligned (((1::word32) + of_nat n << objBitsKO val + us) + ptr) (objBitsKO val + us)") prefer 2 apply (clarsimp simp:field_simps) apply (rule aligned_add_aligned[OF range_cover.aligned],assumption) apply (rule is_aligned_shiftl_self) apply (simp add:range_cover_def) apply (rule monad_eq_split[where Q ="\x s'. s' = s \ ptr && mask (objBitsKO val + us) = 0"]) apply (clarsimp simp:is_aligned_mask[symmetric]) apply (subst new_cap_addrs_fold') apply (drule range_cover_not_zero_shift[rotated,where gbits = us]) apply simp+ apply (simp add:word_le_sub1) apply (subst new_cap_addrs_fold') apply (drule range_cover_le[where n = "Suc n"]) apply simp apply (drule range_cover_not_zero_shift[rotated,where gbits = us]) apply simp+ apply (simp add:word_le_sub1) apply (subst new_cap_addrs_fold') apply (rule word_1_le_power) apply (simp add:range_cover_def) apply (rule monad_eq_split[where Q ="\r s'. r = ksPSpace s \ s' = s"]) apply (rule monad_eq_split2[where Q = "\r s'. s' = s"]) apply (simp add:field_simps) apply (subst no_overlap_check) apply (erule range_cover_le) apply simp+ apply (subst no_overlap_check) apply (erule range_cover_le) apply simp+ apply clarsimp apply (simp add:new_caps_addrs_append[where n = "Suc n",simplified]) apply (subst modify_specify2[where g = return,simplified]) apply (subst modify_specify2) apply (subst modify_specify) apply (simp add:modify_comp) apply (subst monad_commute_simple[OF modify_objs_commute,where g= "\x y. return ()",simplified]) apply (frule range_cover.sz(1)) apply (frule range_cover.sz(2)) apply clarsimp apply (erule new_cap_addrs_disjoint) apply (rule monad_eq_split2[where Q = "\r. pspace_no_overlap' (((1::word32) + of_nat n << objBitsKO val + us) + ptr) (objBitsKO val + us) and pspace_aligned'"]) apply (simp add:shiftl_t2n field_simps) apply (clarsimp simp:unless_True) apply (rule sym) apply (clarsimp simp:gets_def get_def) apply (subst bind_def,simp) apply (subst monad_eq) apply (rule no_overlap_check) apply (erule range_cover_full) apply (simp add:range_cover_def word_bits_def) apply (simp add:field_simps) apply simp+ apply (clarsimp simp:simpler_modify_def) apply wp apply (clarsimp simp del:fun_upd_apply) apply (rule conjI) apply (rule use_valid[OF _ pspace_no_overlap'_modify[where sz = sz]]) apply (simp add:simpler_modify_def) apply (clarsimp simp:field_simps) apply (rule pspace_no_overlap'_le) apply (erule pspace_no_overlap'_tail) apply simp+ apply (simp add:range_cover_def) apply (erule range_cover.sz(1)[where 'a=32, folded word_bits_def]) apply (subst data_map_insert_def[symmetric]) apply (drule(2) retype_aligned_distinct'(2)) prefer 2 apply (simp cong: kernel_state.fold_congs) apply (drule range_cover_le[where n = "Suc n"]) apply simp apply (rule range_cover_le[OF range_cover_rel,OF _ _ _ le_refl]) apply simp+ apply (drule range_cover.unat_of_nat_n_shift[where gbits = us]) apply simp apply simp apply (wp haskell_assert_wp | wpc)+ apply simp apply (wp hoare_unless_wp |clarsimp)+ apply (drule range_cover.aligned) apply (simp add:is_aligned_mask) done lemma placeNewObject_doMachineOp_commute: "monad_commute (K (us < word_bits \ is_aligned ptr (objBitsKO (injectKOS ty) + us) \ objBitsKO (injectKOS ty) + us < word_bits) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ((objBitsKO (injectKOS ty)) + us)) (placeNewObject ptr ty us) (doMachineOp f)" apply (rule commute_name_pre_state) apply (rule monad_commute_guard_imp) apply (rule commute_rewrite [where Q = "pspace_no_overlap' ptr ((objBitsKO (injectKOS ty)) + us) and pspace_aligned'"]) apply (rule simpler_placeNewObject_def; simp) apply (wp doMachineOp_psp_no_overlap) apply (simp add: modify_specify modify_mapM_x) apply (rule commute_commute) apply (rule mapM_x_commute[where f = id]) apply (rule doMachineOp_upd_heap_commute) apply wp apply clarsimp apply (rule new_cap_addrs_distinct[OF range_cover_rel]) apply (erule(1) range_cover_full) apply simp apply simp done lemma doMachineOp_ksArchState_commute: "monad_commute \ (doMachineOp f) (gets (g \ ksArchState))" apply (clarsimp simp:monad_commute_def gets_def return_def get_def bind_def) apply (intro conjI set_eqI iffI) apply (clarsimp simp: doMachineOp_def select_f_def gets_def get_def bind_def return_def simpler_modify_def) apply (erule bexI[rotated]) apply clarsimp apply (clarsimp simp: doMachineOp_def select_f_def gets_def get_def bind_def return_def simpler_modify_def) apply (erule bexI[rotated]) apply clarsimp+ done lemma doMachineOp_copyGlobalMapping_commute: "monad_commute (valid_arch_state' and page_directory_at' r) (doMachineOp f) (copyGlobalMappings r)" apply (clarsimp simp:copyGlobalMappings_def) apply (rule monad_commute_guard_imp) apply (rule monad_commute_split) apply (rule mapM_x_commute[where f = id]) apply (rule monad_commute_split[OF _ getPDE_doMachineOp_commute]) apply (rule doMachineOp_storePDE_commute) apply wp apply clarsimp apply (rule doMachineOp_ksArchState_commute) apply wp apply clarsimp apply (clarsimp simp: valid_arch_state'_def page_directory_at'_def objBits_simps archObjSize_def pdBits_def pageBits_def) apply (drule le_m1_iff_lt[where x = "(0x1000::word32)",simplified,THEN iffD1]) apply (clarsimp) done lemma placeNewObject_old_pd_at': "\page_directory_at' ptr and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr' (objBitsKO (injectKOS val) + sz) and K (is_aligned ptr' (objBitsKO (injectKOS val) + sz) \ objBitsKO (injectKOS val) + sz < word_bits)\ placeNewObject ptr' val sz \\rv. page_directory_at' ptr\" apply (clarsimp simp:placeNewObject_def2 page_directory_at'_def) apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift) apply (wp createObjects'_typ_at) apply clarsimp apply (intro conjI) apply (rule range_cover_full; simp) apply simp+ done lemma createObjects'_page_directory_at': "\K (range_cover ptr sz 14 (Suc n)) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz\ createObjects' ptr (Suc n) (KOArch (KOPDE makeObject)) 12 \\rv s. (\x\of_nat n. page_directory_at' (ptr + (x << 14)) s)\" apply (rule createObjects'_wp_subst) apply simp apply (clarsimp simp:valid_def) apply (frule use_valid[OF _ createObjects_ko_at_strg[where 'b = pde]]) apply (simp add:objBits_simps archObjSize_def) apply simp apply (simp add:projectKO_def projectKO_opt_pde return_def) apply simp apply (clarsimp simp:page_directory_at'_def pdBits_def pageBits_def) apply (intro conjI) apply (rule aligned_add_aligned[OF range_cover.aligned],simp) apply (rule is_aligned_shiftl_self) apply (simp add:range_cover_def) apply (drule_tac x = "ptr + (x << 14)" in bspec) apply (simp add:createObjects_def bind_def return_def) apply (clarsimp simp:objBits_simps archObjSize_def) apply (clarsimp simp:typ_at'_def) apply (drule_tac x = y in spec) apply (simp add:obj_at'_real_def objBits_simps archObjSize_def) apply (erule ko_wp_at'_weakenE) apply (simp add: projectKO_opt_pde) apply (case_tac ko; simp) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object; simp) done lemma gsCNodes_upd_createObjects'_comm: "do _ \ modify (gsCNodes_update f); x \ createObjects' ptr n obj us; m x od = do x \ createObjects' ptr n obj us; _ \ modify (gsCNodes_update f); m x od" apply (rule ext) apply (case_tac x) by (auto simp: createObjects'_def split_def bind_assoc return_def unless_def when_def simpler_gets_def alignError_def fail_def assert_def simpler_modify_def bind_def split: option.splits) lemma gsUserPages_upd_createObjects'_comm: "do _ \ modify (gsUserPages_update f); x \ createObjects' ptr n obj us; m x od = do x \ createObjects' ptr n obj us; _ \ modify (gsUserPages_update f); m x od" apply (rule ext) apply (case_tac x) by (auto simp: createObjects'_def split_def bind_assoc return_def unless_def when_def simpler_gets_def alignError_def fail_def assert_def simpler_modify_def bind_def split: option.splits) (* FIXME: move *) lemma ef_dmo': "empty_fail f \ empty_fail (doMachineOp f)" by (auto simp: empty_fail_def doMachineOp_def split_def select_f_def simpler_modify_def simpler_gets_def return_def bind_def image_def) (* FIXME: move *) lemma dmo'_when_fail_comm: assumes "empty_fail f" shows "doMachineOp f >>= (\x. when P fail >>= (\_. m x)) = when P fail >>= (\_. doMachineOp f >>= m)" apply (rule ext) apply (cut_tac ef_dmo'[OF assms]) apply (auto simp add: empty_fail_def when_def fail_def return_def bind_def split_def image_def, fastforce) done (* FIXME: move *) lemma dmo'_gets_ksPSpace_comm: "doMachineOp f >>= (\_. gets ksPSpace >>= m) = gets ksPSpace >>= (\x. doMachineOp f >>= (\_. m x))" apply (rule ext) apply (auto simp add: doMachineOp_def simpler_modify_def simpler_gets_def return_def select_f_def bind_def split_def image_def) apply (rule_tac x=aa in exI; drule prod_injects; clarsimp) apply (rule_tac x="snd (m (ksPSpace x) (x\ksMachineState := bb\))" in exI, clarsimp) apply (rule_tac x="{(ab, x\ksMachineState := bb\)}" in exI, simp) apply (rule bexI[rotated], assumption, simp) apply (rule_tac x="fst (m (ksPSpace x) (x\ksMachineState := bb\))" in exI, clarsimp) apply (rule_tac x="snd (m (ksPSpace x) (x\ksMachineState := bb\))" in exI, clarsimp) apply (rule_tac x="{(ab, x\ksMachineState := bb\)}" in exI, simp) apply (rule bexI[rotated], assumption, simp) apply (rule_tac x=a in exI, clarsimp) apply (rule_tac x="{(aa, x\ksMachineState := b\)}" in exI, simp) apply (rule bexI[rotated], assumption, simp) apply (rule_tac x=a in exI, clarsimp) apply (rule_tac x="{(aa, x\ksMachineState := b\)}" in exI, simp) apply (rule bexI[rotated], assumption, simp) done lemma dmo'_ksPSpace_update_comm': assumes "empty_fail f" shows "doMachineOp f >>= (\x. modify (ksPSpace_update g) >>= (\_. m x)) = modify (ksPSpace_update g) >>= (\_. doMachineOp f >>= m)" proof - have ksMachineState_ksPSpace_update: "\s. ksMachineState (ksPSpace_update g s) = ksMachineState s" by simp have updates_independent: "\f. ksPSpace_update g \ ksMachineState_update f = ksMachineState_update f \ ksPSpace_update g" by (rule ext) simp from assms show ?thesis apply (simp add: doMachineOp_def split_def bind_assoc) apply (simp add: gets_modify_comm2[OF ksMachineState_ksPSpace_update]) apply (rule arg_cong2[where f=bind, OF refl], rule ext) apply (simp add: empty_fail_def select_f_walk[OF empty_fail_modify] modify_modify_bind updates_independent) done qed lemma dmo'_createObjects'_comm: assumes ef: "empty_fail f" shows "do _ \ doMachineOp f; x \ createObjects' ptr n obj us; m x od = do x \ createObjects' ptr n obj us; _ \ doMachineOp f; m x od" apply (simp add: createObjects'_def bind_assoc split_def unless_def alignError_def dmo'_when_fail_comm[OF ef] dmo'_gets_ksPSpace_comm dmo'_ksPSpace_update_comm'[OF ef, symmetric]) apply (rule arg_cong2[where f=bind, OF refl], rule ext) apply (rule arg_cong2[where f=bind, OF refl], rule ext) apply (rename_tac u w) apply (case_tac "fst (lookupAround2 (ptr + of_nat (shiftL n (objBitsKO obj + us) - Suc 0)) w)", clarsimp+) apply (simp add: assert_into_when dmo'_when_fail_comm[OF ef]) done lemma unless_dmo'_createObjects'_comm: assumes ef: "empty_fail f" shows "do _ \ unless d (doMachineOp f); x \ createObjects' ptr n obj us; m x od = do x \ createObjects' ptr n obj us; _ \ unless d (doMachineOp f); m x od" apply (case_tac d, simp) apply (simp only: unless_False) apply (rule dmo'_createObjects'_comm[OF ef]) done lemma dmo'_gsUserPages_upd_comm: assumes "empty_fail f" shows "doMachineOp f >>= (\x. modify (gsUserPages_update g) >>= (\_. m x)) = modify (gsUserPages_update g) >>= (\_. doMachineOp f >>= m)" proof - have ksMachineState_ksPSpace_update: "\s. ksMachineState (gsUserPages_update g s) = ksMachineState s" by simp have updates_independent: "\f. gsUserPages_update g \ ksMachineState_update f = ksMachineState_update f \ gsUserPages_update g" by (rule ext) simp from assms show ?thesis apply (simp add: doMachineOp_def split_def bind_assoc) apply (simp add: gets_modify_comm2[OF ksMachineState_ksPSpace_update]) apply (rule arg_cong2[where f=bind, OF refl], rule ext) apply (simp add: empty_fail_def select_f_walk[OF empty_fail_modify] modify_modify_bind updates_independent) done qed lemma unless_dmo'_gsUserPages_upd_comm: assumes "empty_fail f" shows "(unless d (doMachineOp f) >>= (\x. modify (gsUserPages_update g) >>= (\_. m x))) = modify (gsUserPages_update g) >>= (\_. unless d (doMachineOp f) >>= m)" apply (case_tac d, simp) apply (simp only: unless_False) apply (rule dmo'_gsUserPages_upd_comm[OF assms]) done lemma rewrite_step: assumes rewrite: "\s. P s \ f s = f' s" shows "P s \ ( f >>= g ) s = (f' >>= g ) s" by (simp add:bind_def rewrite) lemma rewrite_through_step: assumes rewrite: "\s r. P s \ f r s = f' r s" assumes hoare: "\Q\ g \\r. P\" shows "Q s \ (do x \ g; y \ f x; h x y od) s = (do x \ g; y \ f' x; h x y od) s" apply (rule monad_eq_split[where Q = "\r. P"]) apply (simp add:bind_def rewrite) apply (rule hoare) apply simp done lemma threadSet_commute: assumes preserve: "\P and tcb_at' ptr \ f \\r. tcb_at' ptr\" assumes commute: "monad_commute P' f ( modify (ksPSpace_update (\ps. ps(ptr \ case ps ptr of Some (KOTCB tcb) \ KOTCB (tcbDomain_update (\_. r) tcb)))))" shows "monad_commute (tcb_at' ptr and P and P') f (threadSet (tcbDomain_update (\_. r)) ptr)" apply (clarsimp simp add: monad_commute_def) apply (subst rewrite_through_step[where h = "\x y. return (x,())",simplified bind_assoc]) apply (erule threadSet_det) apply (rule preserve) apply simp apply (subst rewrite_step[OF threadSet_det]) apply assumption apply simp using commute apply (simp add:monad_commute_def) done lemma createObjects_setDomain_commute: "monad_commute (\s. range_cover ptr' (objBitsKO (KOTCB makeObject)) (objBitsKO (KOTCB makeObject) + 0) (Suc 0) \ pspace_aligned' s \ pspace_distinct' s \ pspace_no_overlap' ptr' (objBitsKO (KOTCB makeObject)) s \ tcb_at' ptr s \ is_aligned ptr' (objBitsKO (KOTCB makeObject))) (createObjects' ptr' (Suc 0) (KOTCB makeObject) 0) (threadSet (tcbDomain_update (\_. r)) ptr)" apply (rule monad_commute_guard_imp) apply (rule threadSet_commute) apply (wp createObjects_orig_obj_at'[where sz = "(objBitsKO (KOTCB makeObject))"]) apply clarsimp apply assumption apply (simp add:placeNewObject_def2[where val = "makeObject::tcb",simplified,symmetric]) apply (rule placeNewObject_modify_commute) apply (clarsimp simp: objBits_simps typ_at'_def word_bits_def obj_at'_def ko_wp_at'_def projectKO_eq projectKO_opt_tcb) apply (clarsimp split:Structures_H.kernel_object.splits) done lemma createObjects_setDomains_commute: "monad_commute (\s. \x\ set xs. tcb_at' (f x) s \ range_cover ptr (objBitsKO (KOTCB makeObject)) (objBitsKO (KOTCB makeObject)) (Suc 0) \ pspace_aligned' s \ pspace_distinct' s \ pspace_no_overlap' ptr (objBitsKO (KOTCB makeObject)) s \ is_aligned ptr (objBitsKO (KOTCB makeObject))) (mapM_x (threadSet (tcbDomain_update (\_. r))) (map f xs)) (createObjects' ptr (Suc 0) (KOTCB makeObject) 0)" proof (induct xs) case Nil show ?case apply (simp add:monad_commute_def mapM_x_Nil) done next case (Cons x xs) show ?case apply (simp add:mapM_x_Cons) apply (rule monad_commute_guard_imp) apply (rule commute_commute[OF monad_commute_split]) apply (rule commute_commute[OF Cons.hyps]) apply (rule createObjects_setDomain_commute) apply (wp hoare_vcg_ball_lift) apply clarsimp done qed lemma createObjects'_pspace_no_overlap2: "\pspace_no_overlap' (ptr + (1 + of_nat n << gz)) sz and K (gz = (objBitsKO val) + us) and K (range_cover ptr sz gz (Suc (Suc n)) \ ptr \ 0)\ createObjects' ptr (Suc n) val us \\addrs s. pspace_no_overlap' (ptr + (1 + of_nat n << gz)) sz s\" proof - note 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 show ?thesis apply (rule hoare_gen_asm)+ apply (clarsimp simp:createObjects'_def split_def new_cap_addrs_fold') apply (subst new_cap_addrs_fold') apply clarsimp apply (drule range_cover_le[where n = "Suc n"]) apply simp apply (drule_tac gbits = us in range_cover_not_zero_shift[rotated]) apply simp+ apply (simp add:word_le_sub1) apply (wp haskell_assert_wp hoare_unless_wp |wpc |simp add:alignError_def del:fun_upd_apply)+ apply (rule conjI) apply (rule impI) apply (subgoal_tac "pspace_no_overlap' (ptr + (1 + of_nat n << objBitsKO val + us)) sz (s\ksPSpace := foldr (\addr map. map(addr \ val)) (new_cap_addrs (unat (1 + of_nat n << us)) ptr val) (ksPSpace s)\)") apply (intro conjI impI allI) apply assumption+ apply (subst pspace_no_overlap'_def) apply (intro allI impI) apply (subst (asm) foldr_upd_app_if) apply (subst range_cover_tail_mask) apply simp+ apply (clarsimp split:if_splits) apply (drule obj_range'_subset_strong[rotated]) apply (rule range_cover_rel[OF range_cover_le[where n = "Suc n"]],assumption) apply simp+ apply (drule range_cover.unat_of_nat_n_shift [OF range_cover_le[where n = "Suc n"],where gbits = us]) apply simp+ apply (simp add:shiftl_t2n field_simps)+ apply (simp add:obj_range'_def) apply (erule disjoint_subset) apply (clarsimp simp:blah) apply (thin_tac "x \ y" for x y) apply (subst (asm) le_m1_iff_lt[THEN iffD1]) apply (drule_tac range_cover_no_0[rotated,where p = "Suc n"]) apply simp apply simp apply (simp add:field_simps) apply (simp add: power_add[symmetric]) apply (simp add: word_neq_0_conv) apply (simp add: power_add[symmetric] field_simps) apply (frule range_cover_subset[where p = "Suc n"]) apply simp apply simp apply (drule(1) pspace_no_overlapD') apply (subst (asm) range_cover_tail_mask) apply simp+ apply (simp add:word_le_sub1 shiftl_t2n field_simps) apply auto done qed lemma new_cap_addrs_def2: "n < 2 ^ 32 \ new_cap_addrs (Suc n) ptr obj = map (\n. ptr + (n << objBitsKO obj)) [0.e.of_nat n]" by (simp add:new_cap_addrs_def upto_enum_word unat_of_nat Fun.comp_def) lemma createTCBs_tcb_at': "\\s. pspace_aligned' s \ pspace_distinct' s \ pspace_no_overlap' ptr sz s \ range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n) \ createObjects' ptr (Suc n) (KOTCB makeObject) 0 \\rv s. (\x\set [0.e.of_nat n]. tcb_at' (ptr + x * 0x200) s)\" apply (simp add:createObjects'_def split_def alignError_def) apply (wp hoare_unless_wp |wpc)+ apply (subst data_map_insert_def[symmetric])+ apply clarsimp apply (subgoal_tac "(\x\of_nat n. tcb_at' (ptr + x * 0x200) (s\ksPSpace := foldr (\addr. data_map_insert addr (KOTCB makeObject)) (new_cap_addrs (Suc n) ptr (KOTCB makeObject)) (ksPSpace s)\))") apply (subst (asm) new_cap_addrs_def2) apply (drule range_cover.weak) apply simp apply simp apply (clarsimp simp: retype_obj_at_disj') apply (clarsimp simp:projectKO_opt_tcb) apply (clarsimp simp add:new_cap_addrs_def image_def) apply (drule_tac x = "unat x" in bspec) apply (simp add:objBits_simps shiftl_t2n) apply (rule unat_less_helper) apply (rule ccontr) apply simp apply (simp add:objBits_simps shiftl_t2n) done lemma createNewCaps_Cons: assumes cover:"range_cover ptr sz (Types_H.getObjectSize ty us) (Suc (Suc n))" and "valid_pspace' s" "valid_arch_state' s" and "pspace_no_overlap' ptr sz s" and "ptr \ 0" shows "createNewCaps ty ptr (Suc (Suc n)) us d s = (do x \ createNewCaps ty ptr (Suc n) us d; r \ RetypeDecls_H.createObject ty (((1 + of_nat n) << Types_H.getObjectSize ty us) + ptr) us d; return (x @ [r]) od) s" proof - have append :"[0.e.(1::word32) + of_nat n] = [0.e.of_nat n] @ [1 + of_nat n]" using cover apply - apply (frule range_cover_not_zero[rotated]) apply simp apply (frule range_cover.unat_of_nat_n) apply (drule range_cover_le[where n = "Suc n"]) apply simp apply (frule range_cover_not_zero[rotated]) apply simp apply (frule range_cover.unat_of_nat_n) apply (subst upto_enum_red'[where X = "2 + of_nat n",simplified]) apply (simp add:field_simps word_le_sub1) apply clarsimp apply (subst upto_enum_red'[where X = "1 + of_nat n",simplified]) apply (simp add:field_simps word_le_sub1) apply simp done have conj_impI: "\A B C. \C;C\B\ \ B \ C" by simp have suc_of_nat: "(1::word32) + of_nat n = of_nat (1 + n)" by simp have gsUserPages_update[simp]: "\f. (\ks. ks \gsUserPages := f (gsUserPages ks)\) = gsUserPages_update f" by (rule ext) simp have gsCNodes_update[simp]: "\f. (\ks. ks \gsCNodes := f (gsCNodes ks)\) = gsCNodes_update f" by (rule ext) simp have if_eq[simp]: "!!x a b pgsz. (if a = ptr + (1 + of_nat n << b) then Some pgsz else if a \ (\n. ptr + (n << b)) ` {x. x \ of_nat n} then Just pgsz else x a) = (if a \ (\n. ptr + (n << b)) ` {x. x \ 1 + of_nat n} then Just pgsz else x a)" apply (simp only: Just_def if3_fold2) apply (rule_tac x="x a" in fun_cong) apply (rule arg_cong2[where f=If, OF _ refl]) apply (subgoal_tac "{x. x \ (1::word32) + of_nat n} = {1 + of_nat n} \ {x. x \ of_nat n}") apply (simp add: add.commute) apply safe apply (clarsimp simp: word_le_less_eq[of _ "1 + of_nat n"]) apply (metis plus_one_helper add.commute) using cover apply - apply (drule range_cover_le[where n = "Suc n"], simp) apply (simp only: suc_of_nat word_le_nat_alt Suc_eq_plus1) apply (frule range_cover.unat_of_nat_n) apply simp apply (drule range_cover_le[where n=n], simp) apply (frule range_cover.unat_of_nat_n, simp) done show ?thesis using assms apply (clarsimp simp:valid_pspace'_def) apply (frule range_cover.aligned) apply (frule(3) pspace_no_overlap'_tail) apply simp apply (drule_tac ptr = "ptr + x" for x in pspace_no_overlap'_le[where sz' = "Types_H.getObjectSize ty us"]) apply (simp add:range_cover_def word_bits_def) apply (erule range_cover.sz(1)[where 'a=32, folded word_bits_def]) apply (simp add: createNewCaps_def) apply (case_tac ty) apply (simp add: ARM_H.toAPIType_def Arch_createNewCaps_def) apply (rename_tac apiobject_type) apply (case_tac apiobject_type) apply (simp_all add: bind_assoc ARM_H.toAPIType_def ) -- Untyped apply (simp add: cteSizeBits_def pageBits_def tcbBlockSizeBits_def epSizeBits_def ntfnSizeBits_def pdBits_def bind_assoc getObjectSize_def ARM_H.getObjectSize_def mapM_def sequence_def Retype_H.createObject_def ARM_H.toAPIType_def createObjects_def ARM_H.createObject_def Arch_createNewCaps_def comp_def apiGetObjectSize_def shiftl_t2n field_simps shiftL_nat mapM_x_def sequence_x_def append fromIntegral_def integral_inv[unfolded Fun.comp_def]) -- "TCB, EP, NTFN" apply (simp add: cteSizeBits_def pageBits_def tcbBlockSizeBits_def epSizeBits_def ntfnSizeBits_def pdBits_def bind_assoc getObjectSize_def ARM_H.getObjectSize_def sequence_def Retype_H.createObject_def ARM_H.toAPIType_def createObjects_def ARM_H.createObject_def Arch_createNewCaps_def comp_def apiGetObjectSize_def shiftl_t2n field_simps shiftL_nat append mapM_x_append2 fromIntegral_def integral_inv[unfolded Fun.comp_def])+ apply (subst monad_eq) apply (rule createObjects_Cons) apply (simp add: field_simps shiftl_t2n bind_assoc pageBits_def objBits_simps placeNewObject_def2)+ apply (rule_tac Q = "\r s. pspace_aligned' s \ pspace_distinct' s \ pspace_no_overlap' (ptr + (0x200 + of_nat n * 0x200)) (objBitsKO (KOTCB makeObject)) s \ range_cover (ptr + 0x200) sz (objBitsKO (KOTCB makeObject)) (Suc n) \ (\x\set [0.e.of_nat n]. tcb_at' (ptr + x * 0x200) s)" in monad_eq_split2) apply simp apply (subst monad_commute_simple[symmetric]) apply (rule commute_commute[OF curDomain_commute]) apply wp apply (rule_tac Q = "\r s. r = (ksCurDomain s) \ pspace_aligned' s \ pspace_distinct' s \ pspace_no_overlap' (ptr + (0x200 + of_nat n * 0x200)) (objBitsKO (KOTCB makeObject)) s \ range_cover (ptr + 0x200) sz (objBitsKO (KOTCB makeObject)) (Suc n) \ (\x\set [0.e.of_nat n]. tcb_at' (ptr + x * 0x200) s) " in monad_eq_split) apply (subst monad_commute_simple[symmetric]) apply (rule createObjects_setDomains_commute) apply (clarsimp simp:objBits_simps) apply (rule conj_impI) apply (erule aligned_add_aligned) apply (rule aligned_add_aligned[where n = 9]) apply (simp add:is_aligned_def) apply (cut_tac is_aligned_shift[where m = 9 and k = "of_nat n", unfolded shiftl_t2n,simplified]) apply (simp add:field_simps)+ apply (erule range_cover_full) apply (simp add:word_bits_conv) apply (rule_tac Q = "\x s. (ksCurDomain s) = ra" in monad_eq_split2) apply simp apply (rule_tac Q = "\x s. (ksCurDomain s) = ra" in monad_eq_split) apply (subst rewrite_step[where f = curDomain and P ="\s. ksCurDomain s = ra" and f' = "return ra"]) apply (simp add:curDomain_def bind_def gets_def get_def) apply simp apply (simp add:mapM_x_singleton) apply wp apply simp apply (wp mapM_x_wp') apply simp apply (simp add:curDomain_def,wp) apply simp apply (wp createObjects'_psp_aligned[where sz = sz] createObjects'_psp_distinct[where sz = sz]) apply (rule hoare_vcg_conj_lift) apply (rule hoare_post_imp[OF _ createObjects'_pspace_no_overlap [unfolded shiftl_t2n,where gz = 9 and sz = sz,simplified]]) apply (simp add:objBits_simps field_simps) apply (simp add: objBits_simps) apply (wp createTCBs_tcb_at'[where sz = sz]) apply (clarsimp simp:objBits_simps word_bits_def field_simps) apply (frule range_cover_le[where n = "Suc n"],simp+) apply (drule range_cover_offset[where p = 1,rotated]) apply simp apply simp apply (((simp add: cteSizeBits_def pageBits_def tcbBlockSizeBits_def epSizeBits_def ntfnSizeBits_def pdBits_def bind_assoc getObjectSize_def ARM_H.getObjectSize_def mapM_def sequence_def Retype_H.createObject_def ARM_H.toAPIType_def createObjects_def ARM_H.createObject_def Arch_createNewCaps_def comp_def apiGetObjectSize_def shiftl_t2n field_simps shiftL_nat mapM_x_def sequence_x_def append fromIntegral_def integral_inv[unfolded Fun.comp_def])+ , subst monad_eq, rule createObjects_Cons , (simp add: field_simps shiftl_t2n bind_assoc pageBits_def objBits_simps placeNewObject_def2)+)+)[2] -- CNode apply (simp add: cteSizeBits_def pageBits_def tcbBlockSizeBits_def epSizeBits_def ntfnSizeBits_def pdBits_def bind_assoc getObjectSize_def ARM_H.getObjectSize_def mapM_def sequence_def Retype_H.createObject_def ARM_H.toAPIType_def createObjects_def ARM_H.createObject_def Arch_createNewCaps_def comp_def apiGetObjectSize_def shiftl_t2n field_simps shiftL_nat mapM_x_def sequence_x_def append fromIntegral_def integral_inv[unfolded Fun.comp_def])+ apply (subst monad_eq, rule createObjects_Cons) apply (simp add: field_simps shiftl_t2n bind_assoc pageBits_def objBits_simps placeNewObject_def2)+ apply (subst gsCNodes_update gsCNodes_upd_createObjects'_comm)+ apply (simp add: modify_modify_bind) apply (rule fun_cong[where x=s]) apply (rule arg_cong2[where f=bind, OF refl ext])+ apply (rule arg_cong2[where f=bind, OF _ refl]) apply (rule arg_cong[where f=modify, OF ext], simp) apply (rule arg_cong2[where f=gsCNodes_update, OF ext refl]) apply (rule ext) apply simp -- "SmallPageObject" apply (simp add: Arch_createNewCaps_def Retype_H.createObject_def createObjects_def bind_assoc ARM_H.toAPIType_def ARM_H.toAPIType_def ARM_H.createObject_def placeNewDataObject_def) apply (intro conjI impI) apply (subst monad_eq, rule createObjects_Cons) apply (simp_all add: field_simps shiftl_t2n pageBits_def getObjectSize_def ARM_H.getObjectSize_def objBits_simps)[6] apply (simp add: bind_assoc placeNewObject_def2 objBits_simps getObjectSize_def ARM_H.getObjectSize_def pageBits_def add.commute append) apply ((subst gsUserPages_update gsCNodes_update gsUserPages_upd_createObjects'_comm unless_dmo'_gsUserPages_upd_comm unless_dmo'_createObjects'_comm dmo'_createObjects'_comm dmo'_gsUserPages_upd_comm | simp add: modify_modify_bind o_def)+)[1] apply (subst monad_eq, rule createObjects_Cons) apply (simp_all add: field_simps shiftl_t2n pageBits_def getObjectSize_def ARM_H.getObjectSize_def objBits_simps)[6] apply (simp add: bind_assoc placeNewObject_def2 objBits_simps getObjectSize_def ARM_H.getObjectSize_def pageBits_def add.commute append) apply (subst gsUserPages_update gsCNodes_update gsUserPages_upd_createObjects'_comm unless_dmo'_gsUserPages_upd_comm unless_dmo'_createObjects'_comm dmo'_createObjects'_comm dmo'_gsUserPages_upd_comm | simp add: modify_modify_bind o_def)+ -- "LargePageObject" apply (simp add: Arch_createNewCaps_def Retype_H.createObject_def createObjects_def bind_assoc ARM_H.toAPIType_def ARM_H.toAPIType_def ARM_H.createObject_def placeNewDataObject_def) apply (intro conjI impI) apply (subst monad_eq, rule createObjects_Cons) apply (simp_all add: field_simps shiftl_t2n pageBits_def getObjectSize_def ARM_H.getObjectSize_def objBits_simps)[6] apply (simp add: bind_assoc placeNewObject_def2 objBits_simps getObjectSize_def ARM_H.getObjectSize_def pageBits_def add.commute append) apply ((subst gsUserPages_update gsCNodes_update gsUserPages_upd_createObjects'_comm unless_dmo'_gsUserPages_upd_comm unless_dmo'_createObjects'_comm dmo'_createObjects'_comm dmo'_gsUserPages_upd_comm | simp add: modify_modify_bind o_def)+)[1] apply (subst monad_eq, rule createObjects_Cons) apply (simp_all add: field_simps shiftl_t2n pageBits_def getObjectSize_def ARM_H.getObjectSize_def objBits_simps)[6] apply (simp add: bind_assoc placeNewObject_def2 objBits_simps ARM_H.getObjectSize_def pageBits_def add.commute append) apply (subst gsUserPages_update gsCNodes_update gsUserPages_upd_createObjects'_comm unless_dmo'_gsUserPages_upd_comm unless_dmo'_createObjects'_comm dmo'_createObjects'_comm dmo'_gsUserPages_upd_comm | simp add: modify_modify_bind o_def)+ -- "SectionObject" apply (simp add: Arch_createNewCaps_def Retype_H.createObject_def createObjects_def bind_assoc toAPIType_def ARM_H.toAPIType_def ARM_H.createObject_def placeNewDataObject_def) apply (intro conjI impI) apply (subst monad_eq, rule createObjects_Cons) apply (simp_all add: field_simps shiftl_t2n pageBits_def getObjectSize_def ARM_H.getObjectSize_def objBits_simps)[6] apply (simp add: bind_assoc placeNewObject_def2 objBits_simps getObjectSize_def ARM_H.getObjectSize_def pageBits_def add.commute append) apply ((subst gsUserPages_update gsCNodes_update gsUserPages_upd_createObjects'_comm unless_dmo'_gsUserPages_upd_comm unless_dmo'_createObjects'_comm dmo'_createObjects'_comm dmo'_gsUserPages_upd_comm | simp add: modify_modify_bind o_def)+)[1] apply (subst monad_eq, rule createObjects_Cons) apply (simp_all add: field_simps shiftl_t2n pageBits_def getObjectSize_def ARM_H.getObjectSize_def objBits_simps)[6] apply (simp add: bind_assoc placeNewObject_def2 objBits_simps ARM_H.getObjectSize_def pageBits_def add.commute append) apply (subst gsUserPages_update gsCNodes_update gsUserPages_upd_createObjects'_comm unless_dmo'_gsUserPages_upd_comm unless_dmo'_createObjects'_comm dmo'_createObjects'_comm dmo'_gsUserPages_upd_comm | simp add: modify_modify_bind o_def)+ -- "SuperSectionObject" apply (simp add: Arch_createNewCaps_def Retype_H.createObject_def createObjects_def bind_assoc toAPIType_def ARM_H.toAPIType_def ARM_H.createObject_def placeNewDataObject_def) apply (intro conjI impI) apply (subst monad_eq, rule createObjects_Cons) apply (simp_all add: field_simps shiftl_t2n pageBits_def getObjectSize_def ARM_H.getObjectSize_def objBits_simps)[6] apply (simp add: bind_assoc placeNewObject_def2 objBits_simps getObjectSize_def ARM_H.getObjectSize_def pageBits_def add.commute append) apply ((subst gsUserPages_update gsCNodes_update gsUserPages_upd_createObjects'_comm unless_dmo'_gsUserPages_upd_comm unless_dmo'_createObjects'_comm dmo'_createObjects'_comm dmo'_gsUserPages_upd_comm | simp add: modify_modify_bind o_def)+)[1] apply (subst monad_eq, rule createObjects_Cons) apply (simp_all add: field_simps shiftl_t2n pageBits_def getObjectSize_def ARM_H.getObjectSize_def objBits_simps)[6] apply (simp add: bind_assoc placeNewObject_def2 objBits_simps ARM_H.getObjectSize_def pageBits_def add.commute append) apply (subst gsUserPages_update gsCNodes_update gsUserPages_upd_createObjects'_comm unless_dmo'_gsUserPages_upd_comm unless_dmo'_createObjects'_comm dmo'_createObjects'_comm dmo'_gsUserPages_upd_comm | simp add: modify_modify_bind o_def)+ -- "PageTableObject" apply (simp add:Arch_createNewCaps_def Retype_H.createObject_def createObjects_def bind_assoc ARM_H.toAPIType_def ARM_H.createObject_def) apply (subst monad_eq,rule createObjects_Cons) apply ((simp add: field_simps shiftl_t2n pageBits_def archObjSize_def getObjectSize_def ARM_H.getObjectSize_def objBits_simps ptBits_def)+)[6] apply (simp add:bind_assoc placeNewObject_def2) apply (simp add: pageBits_def field_simps getObjectSize_def ptBits_def archObjSize_def ARM_H.getObjectSize_def placeNewObject_def2 objBits_simps append) -- "PageDirectoryObject" apply (simp add:Arch_createNewCaps_def Retype_H.createObject_def createObjects_def bind_assoc ARM_H.toAPIType_def ARM_H.createObject_def) apply (subgoal_tac "distinct (map (\n. ptr + (n << 14)) [0.e.((of_nat n)::word32)])") prefer 2 apply (clarsimp simp:objBits_simps archObjSize_def pdBits_def pageBits_def getObjectSize_def ARM_H.getObjectSize_def) apply (subst upto_enum_word) apply (clarsimp simp:distinct_map) apply (frule range_cover.range_cover_n_le) apply (frule range_cover.range_cover_n_less) apply (rule conjI) apply (clarsimp simp:inj_on_def) apply (rule ccontr) apply (erule_tac bnd = "2^(word_bits - 14)" in shift_distinct_helper[rotated 3]) apply simp apply (simp add:word_bits_def) apply (erule less_le_trans[OF word_of_nat_less]) apply (simp add: word_of_nat_le word_bits_def) apply (erule less_le_trans[OF word_of_nat_less]) apply (simp add:word_of_nat_le word_bits_def) apply (frule range_cover.unat_of_nat_n[OF range_cover_le[where n = n]]) apply simp apply (rule ccontr) apply simp apply (drule of_nat_inj32[THEN iffD1,rotated -1]) apply (simp_all add: word_bits_def)[3] apply (clarsimp) apply (erule_tac bnd = "2^(word_bits - 14)" in shift_distinct_helper[rotated 3]) apply simp apply (simp add:word_bits_def) apply (simp add:word_of_nat_less word_bits_def) apply (erule less_le_trans[OF word_of_nat_less]) apply (simp add:word_of_nat_le word_bits_def) apply (rule ccontr) apply (frule range_cover.unat_of_nat_n[OF range_cover_le[where n = n]]) apply simp apply simp apply (drule of_nat_inj32[THEN iffD1,rotated -1]) apply (simp_all add: word_bits_def)[3] apply (subst monad_eq,rule createObjects_Cons) apply ((simp add: field_simps shiftl_t2n pageBits_def archObjSize_def getObjectSize_def ARM_H.getObjectSize_def pdBits_def objBits_simps ptBits_def)+)[6] apply (simp add:objBits_simps archObjSize_def pdBits_def pageBits_def getObjectSize_def ARM_H.getObjectSize_def) apply (simp add:bind_assoc) apply (simp add: placeNewObject_def2[where val = "makeObject::ARM_H.pde",simplified,symmetric]) apply (rule_tac Q = "\r s. valid_arch_state' s \ (\x\of_nat n. page_directory_at' (ptr + (x << 14)) s) \ Q s" for Q in monad_eq_split) apply (rule sym) apply (subst bind_assoc[symmetric]) apply (subst monad_commute_simple) apply (rule commute_commute[OF monad_commute_split]) apply (rule placeNewObject_doMachineOp_commute) apply (rule mapM_x_commute[where f = id]) apply (rule placeNewObject_copyGlobalMapping_commute) apply (wp copyGlobalMappings_pspace_no_overlap' mapM_x_wp'| clarsimp)+ apply (clarsimp simp:objBits_simps archObjSize_def pdBits_def pageBits_def word_bits_conv) apply assumption (* resolve assumption , yuck *) apply (simp add:append mapM_x_append bind_assoc) apply (rule monad_eq_split[where Q = "\ r s. pspace_aligned' s \ pspace_distinct' s \ valid_arch_state' s \ (\r \ of_nat n. page_directory_at' (ptr + (r << 14)) s) \ page_directory_at' (ptr + ((1 + of_nat n) << 14)) s"]) apply (rule monad_eq_split[where Q = "\ r s. pspace_aligned' s \ pspace_distinct' s \ valid_arch_state' s \ (\r \ of_nat n. page_directory_at' (ptr + (r << 14)) s) \ page_directory_at' (ptr + ((1 + of_nat n) << 14)) s"]) apply (subst monad_commute_simple) apply (rule doMachineOp_copyGlobalMapping_commute) apply (clarsimp simp:field_simps) apply (simp add:field_simps mapM_x_singleton) apply (rule monad_eq_split[where Q = "\ r s. pspace_aligned' s \ pspace_distinct' s \ valid_arch_state' s \ page_directory_at' (ptr + (1 + of_nat n << 14)) s"]) apply (subst doMachineOp_bind) apply (wp empty_fail_mapM_x empty_fail_cleanCacheRange_PoU) apply (simp add:bind_assoc objBits_simps field_simps archObjSize_def shiftL_nat) apply wp apply simp apply (rule mapM_x_wp') apply (rule hoare_pre) apply (wp copyGlobalMappings_pspace_no_overlap' | clarsimp)+ apply (clarsimp simp:page_directory_at'_def) apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift) apply ((clarsimp simp:page_directory_at'_def)+)[2] apply (wp placeNewObject_pspace_aligned' placeNewObject_pspace_distinct') apply (simp add:placeNewObject_def2 field_simps) apply (rule hoare_vcg_conj_lift) apply (rule createObjects'_wp_subst) apply (wp createObjects_valid_arch[where sz = 14]) apply (rule hoare_vcg_conj_lift) apply (clarsimp simp:page_directory_at'_def) apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift createObjects'_typ_at[where sz = 14]) apply (rule hoare_strengthen_post[OF createObjects'_page_directory_at'[where sz = 14]]) apply simp apply (clarsimp simp:objBits_simps page_directory_at'_def field_simps archObjSize_def word_bits_conv range_cover_full aligned_add_aligned range_cover.aligned is_aligned_shiftl_self) apply (frule pspace_no_overlap'_le2[where ptr' = "(ptr + (1 + of_nat n << 14))"]) apply (subst shiftl_t2n,subst mult.commute, subst suc_of_nat) apply (rule order_trans[OF range_cover_bound,where n1 = "1 + n"]) apply (erule range_cover_le,simp) apply simp apply (rule word_sub_1_le) apply (drule(1) range_cover_no_0[where p = "n+1"]) apply simp apply simp apply (erule(1) range_cover_tail_mask) apply (rule hoare_vcg_conj_lift) apply (rule createObjects'_wp_subst) apply (wp createObjects_valid_arch[where sz = sz]) apply (wp createObjects'_page_directory_at'[where sz = sz] createObjects'_psp_aligned[where sz = sz] createObjects'_psp_distinct[where sz = sz] hoare_vcg_imp_lift createObjects'_pspace_no_overlap[where sz = sz] | simp add:objBits_simps archObjSize_def field_simps)+ apply (drule range_cover_le[where n = "Suc n"]) apply simp apply (clarsimp simp:word_bits_def valid_pspace'_def) apply (clarsimp simp:aligned_add_aligned[OF range_cover.aligned] is_aligned_shiftl_self word_bits_def)+ done qed lemma createObject_def2: "(RetypeDecls_H.createObject ty ptr us dev >>= (\x. return [x])) = createNewCaps ty ptr (Suc 0) us dev" apply (clarsimp simp:createObject_def createNewCaps_def placeNewObject_def2) apply (case_tac ty) apply (simp_all add: toAPIType_def) defer apply ((clarsimp simp: Arch_createNewCaps_def createObjects_def shiftL_nat ARM_H.createObject_def placeNewDataObject_def placeNewObject_def2 objBits_simps bind_assoc clearMemory_def clearMemoryVM_def fun_upd_def[symmetric] word_size mapM_x_singleton storeWordVM_def)+)[6] apply (rename_tac apiobject_type) apply (case_tac apiobject_type) apply (clarsimp simp: Arch_createNewCaps_def createObjects_def shiftL_nat ARM_H.createObject_def placeNewObject_def2 objBits_simps bind_assoc clearMemory_def clearMemoryVM_def word_size mapM_x_singleton storeWordVM_def)+ done lemma createNewObjects_def2: "\dslots \ []; length ( dslots ) < 2^word_bits; cte_wp_at' (\c. isUntypedCap (cteCap c)) parent s; \slot \ set dslots. cte_wp_at' (\c. cteCap c = capability.NullCap) slot s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; caps_overlap_reserved' {ptr..ptr + of_nat (length dslots) * 2 ^ Types_H.getObjectSize ty us - 1} s; valid_pspace' s; distinct dslots; valid_arch_state' s; range_cover ptr sz (Types_H.getObjectSize ty us) (length dslots); ptr \ 0; ksCurDomain s \ maxDomain\ \ createNewObjects ty parent dslots ptr us d s = insertNewCaps ty parent dslots ptr us d s" apply (clarsimp simp:insertNewCaps_def createNewObjects_def neq_Nil_conv) proof - fix y ys have list_inc: "\n. [0.e.Suc n] = [0 .e. n] @ [n+1]" by simp assume le: "Suc (length (ys::word32 list)) < 2 ^ word_bits" assume list_nc: "\slot \ set ys. cte_wp_at' (\c. cteCap c = capability.NullCap) slot s" assume dist: "distinct ys" assume extra: "y\ set ys" "cte_wp_at' (\c. cteCap c = capability.NullCap) y s" assume not_0: "ptr \ 0" assume kscd: "ksCurDomain s \ maxDomain" assume valid_psp: "valid_pspace' s" assume valid_arch_state: "valid_arch_state' s" assume psp_no_overlap: "pspace_no_overlap' ptr sz s" assume caps_no_overlap: "caps_no_overlap'' ptr sz s" assume caps_reserved: "caps_overlap_reserved' {ptr..ptr + (1 + of_nat (length ys)) * 2 ^ (Types_H.getObjectSize ty us) - 1} s" assume range_cover: "range_cover ptr sz (Types_H.getObjectSize ty us) (Suc (length ys))" assume unt_at: "cte_wp_at' (\c. isUntypedCap (cteCap c)) parent s" show "zipWithM_x (\num slot. RetypeDecls_H.createObject ty ((num << Types_H.getObjectSize ty us) + ptr) us d >>= insertNewCap parent slot) [0.e.of_nat (length ys)] (y # ys) s = (createNewCaps ty ptr (Suc (length ys)) us d >>= zipWithM_x (insertNewCap parent) (y # ys)) s" using le list_nc dist extra range_cover not_0 caps_reserved proof (induct ys arbitrary: y rule:rev_induct) case Nil show ?case by (clarsimp simp:zipWithM_x_def zipWith_def sequence_x_def createObject_def2[symmetric]) next case (snoc a as b) have caps_r:"caps_overlap_reserved' {ptr..ptr + (1 + of_nat (length as)) * 2 ^ Types_H.getObjectSize ty us - 1} s" using snoc.prems apply - apply (erule caps_overlap_reserved'_subseteq) apply (cut_tac is_aligned_no_overflow [where ptr = "ptr + ((1 + of_nat (length as)) << APIType_capBits ty us)" and sz = " Types_H.getObjectSize ty us"]) apply (clarsimp simp: power_add[symmetric] shiftl_t2n field_simps objSize_eq_capBits ) apply (rule order_trans[OF word_sub_1_le]) apply (drule(1) range_cover_no_0[where p = "Suc (length as)"]) apply simp apply (simp add:word_arith_nat_Suc power_add[symmetric] field_simps) apply (simp add:shiftl_t2n) apply (rule aligned_add_aligned[OF range_cover.aligned]) apply (simp add:objSize_eq_capBits)+ apply (rule is_aligned_shiftl_self) apply (simp add:range_cover_def objSize_eq_capBits)+ done show ?case apply simp using snoc.prems apply (subst upto_enum_inc_1) apply (rule word_of_nat_less) apply (simp add:word_bits_def minus_one_norm) apply (subst append_Cons[symmetric]) apply (subst zipWithM_x_append1) apply (clarsimp simp:unat_of_nat32 bind_assoc) apply (subst monad_eq) apply (rule snoc.hyps) apply (simp add:caps_r | rule range_cover_le)+ apply (simp add:snoc.hyps bind_assoc) apply (rule sym) apply (subst monad_eq) apply (erule createNewCaps_Cons[OF _ valid_psp valid_arch_state psp_no_overlap not_0]) apply (rule sym) apply (simp add:bind_assoc del:upto_enum_nat) apply (rule_tac Q = "(\r s. (\cap\set r. cap \ capability.NullCap) \ cte_wp_at' (\c. isUntypedCap (cteCap c)) parent s \ cte_wp_at' (\c. cteCap c = capability.NullCap) b s \ (\slot\set as. cte_wp_at' (\c. cteCap c = capability.NullCap) slot s) \ pspace_no_overlap' (ptr + (1 + of_nat (length as) << Types_H.getObjectSize ty us)) (Types_H.getObjectSize ty us) s \ valid_pspace' s \ valid_arch_state' s \ Q r s)" for Q in monad_eq_split) apply (subst append_Cons[symmetric]) apply (subst zipWithM_x_append1) apply clarsimp apply assumption apply (clarsimp simp:field_simps) apply (subst monad_commute_simple[OF commute_commute]) apply (rule new_cap_object_commute) apply (clarsimp) apply (frule_tac p = "1 + length as" in range_cover_no_0[rotated]) apply clarsimp apply simp apply (subst (asm) Abs_fnat_hom_add[symmetric]) apply (intro conjI) apply (simp add:range_cover_def word_bits_def) apply (rule aligned_add_aligned[OF range_cover.aligned],simp) apply (rule is_aligned_shiftl_self) apply (simp add:range_cover_def) apply (simp add:range_cover_def) apply (clarsimp simp:field_simps shiftl_t2n) apply (clarsimp simp:createNewCaps_def) apply (wp createNewCaps_not_nc createNewCaps_pspace_no_overlap'[where sz = sz] createNewCaps_cte_wp_at'[where sz = sz] hoare_vcg_ball_lift createNewCaps_valid_pspace[where sz = sz] createNewCaps_obj_at'[where sz=sz]) apply simp apply (rule range_cover_le) apply (simp add:objSize_eq_capBits caps_r)+ apply (wp createNewCaps_ret_len createNewCaps_valid_arch_state) apply (frule range_cover_le[where n = "Suc (length as)"]) apply simp+ using psp_no_overlap caps_r valid_psp unt_at caps_no_overlap valid_arch_state apply (clarsimp simp: valid_pspace'_def objSize_eq_capBits) apply (auto simp: kscd) done qed qed lemma createNewObjects_corres_helper: assumes check: "distinct dslots" and cover: "range_cover ptr sz (Types_H.getObjectSize ty us) (length dslots)" and not_0: "ptr \ 0" "length dslots \ 0" and c: "corres r P P' f (insertNewCaps ty parent dslots ptr us d)" and imp: "\s. P' s \ (cte_wp_at' (\c. isUntypedCap (cteCap c)) parent s \ (\slot \ set dslots. cte_wp_at' (\c. cteCap c = capability.NullCap) slot s) \ pspace_no_overlap' ptr sz s \ caps_no_overlap'' ptr sz s \ caps_overlap_reserved' {ptr..ptr + of_nat (length dslots) * 2^ (Types_H.getObjectSize ty us) - 1} s \ valid_pspace' s \ valid_arch_state' s \ ksCurDomain s \ maxDomain)" shows "corres r P P' f (createNewObjects ty parent dslots ptr us d)" using check cover not_0 apply (clarsimp simp:corres_underlying_def) apply (frule imp) apply (frule range_cover.range_cover_le_n_less(1)[where 'a=32, folded word_bits_def, OF _ le_refl]) apply clarsimp apply (simp add:createNewObjects_def2) using c apply (clarsimp simp:corres_underlying_def) apply (drule(1) bspec) apply clarsimp done lemma createNewObjects_wp_helper: assumes check: "distinct dslots" and cover: "range_cover ptr sz (Types_H.getObjectSize ty us) (length dslots)" and not_0: "ptr \ 0" "length dslots \ 0" shows "\P\ insertNewCaps ty parent dslots ptr us d \Q\ \ \P and (cte_wp_at' (\c. isUntypedCap (cteCap c)) parent and (\s. \slot \ set dslots. cte_wp_at' (\c. cteCap c = capability.NullCap) slot s) and pspace_no_overlap' ptr sz and caps_no_overlap'' ptr sz and valid_pspace' and valid_arch_state' and caps_overlap_reserved' {ptr..ptr + of_nat (length dslots) * 2^ (Types_H.getObjectSize ty us) - 1} and (\s. ksCurDomain s \ maxDomain)) \ (createNewObjects ty parent dslots ptr us d) \Q\" using assms apply (clarsimp simp:valid_def) apply (drule_tac x = s in spec) apply (frule range_cover.range_cover_le_n_less(1)[where 'a=32, folded word_bits_def, OF _ le_refl]) apply (simp add:createNewObjects_def2[symmetric]) apply (drule(1) bspec) apply clarsimp done lemma createObject_def3: "createObject = (\ty ptr us d. createNewCaps ty ptr (Suc 0) us d >>= (\m. return (hd m)))" apply (rule ext)+ apply (simp add:createObject_def2[symmetric]) done lemma ArchCreateObject_pspace_no_overlap': "\\s. pspace_no_overlap' (ptr + (of_nat n << APIType_capBits ty userSize)) sz s \ pspace_aligned' s \ pspace_distinct' s \ range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \ ptr \ 0\ ARM_H.createObject ty (ptr + (of_nat n << APIType_capBits ty userSize)) userSize d \\archCap. pspace_no_overlap' (ptr + (1 + of_nat n << APIType_capBits ty userSize)) sz\" apply (rule hoare_pre) apply (clarsimp simp:ARM_H.createObject_def) apply wpc apply (wp doMachineOp_psp_no_overlap unless_doMachineOp_psp_no_overlap[simplified] createObjects'_pspace_no_overlap2 hoare_when_weak_wp copyGlobalMappings_pspace_no_overlap' createObjects'_psp_aligned[where sz = sz] createObjects'_psp_distinct[where sz = sz] | simp add: placeNewObject_def2 word_shiftl_add_distrib | simp add: placeNewObject_def2 word_shiftl_add_distrib | simp add: placeNewDataObject_def placeNewObject_def2 word_shiftl_add_distrib field_simps split del: if_splits | clarsimp simp add: add.assoc[symmetric],wp createObjects'_pspace_no_overlap2[where n =0 and sz = sz,simplified] | clarsimp simp add: APIType_capBits_def objBits_simps pageBits_def)+ apply (clarsimp simp: conj_comms) apply (frule(1) range_cover_no_0[where p = n]) apply simp apply (subgoal_tac "is_aligned (ptr + (of_nat n << APIType_capBits ty userSize)) (APIType_capBits ty userSize) ") prefer 2 apply (rule aligned_add_aligned[OF range_cover.aligned],assumption) apply (simp add:is_aligned_shiftl_self range_cover_sz') apply (simp add: APIType_capBits_def) apply (frule range_cover_offset[rotated,where p = n]) apply simp+ apply (frule range_cover_le[where n = "Suc (Suc 0)"]) apply simp apply (frule pspace_no_overlap'_le2) apply (rule range_cover_compare_offset) apply simp+ apply (clarsimp simp:word_shiftl_add_distrib ,simp add:field_simps) apply (clarsimp simp:add.assoc[symmetric]) apply (rule range_cover_tail_mask[where n =0,simplified]) apply (drule range_cover_offset[rotated,where p = n]) apply simp apply (clarsimp simp:shiftl_t2n field_simps) apply (metis numeral_2_eq_2) apply (simp add:shiftl_t2n field_simps) apply (intro conjI allI) apply (clarsimp simp:field_simps pageBits_def pdBits_def word_bits_conv archObjSize_def ptBits_def APIType_capBits_def shiftl_t2n objBits_simps | rule conjI | erule range_cover_le,simp)+ done lemma to_from_apiTypeD: "toAPIType ty = Some x \ ty = fromAPIType x" by (cases ty) (auto simp add: fromAPIType_def toAPIType_def) lemma createObject_pspace_no_overlap': "\\s. pspace_no_overlap' (ptr + (of_nat n << APIType_capBits ty userSize)) sz s \ pspace_aligned' s \ pspace_distinct' s \ range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \ ptr \ 0\ createObject ty (ptr + (of_nat n << APIType_capBits ty userSize)) userSize d \\rv s. pspace_no_overlap' (ptr + (1 + of_nat n << APIType_capBits ty userSize)) sz s\" apply (rule hoare_pre) apply (clarsimp simp:createObject_def) apply wpc apply (wp ArchCreateObject_pspace_no_overlap') apply wpc apply wp apply (simp add:placeNewObject_def2) apply (wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap2 unless_doMachineOp_psp_no_overlap[simplified] | simp add: placeNewObject_def2 curDomain_def word_shiftl_add_distrib field_simps)+ apply (simp add:add.assoc[symmetric]) apply (wp createObjects'_pspace_no_overlap2 [where n =0 and sz = sz,simplified]) apply (simp add:placeNewObject_def2) apply (wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap2 unless_doMachineOp_psp_no_overlap[simplified] | simp add: placeNewObject_def2 word_shiftl_add_distrib field_simps)+ apply (simp add:add.assoc[symmetric]) apply (wp createObjects'_pspace_no_overlap2 [where n =0 and sz = sz,simplified]) apply (simp add:placeNewObject_def2) apply (wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap2 unless_doMachineOp_psp_no_overlap[simplified] | simp add: placeNewObject_def2 word_shiftl_add_distrib field_simps)+ apply (simp add:add.assoc[symmetric]) apply (wp createObjects'_pspace_no_overlap2 [where n =0 and sz = sz,simplified]) apply (simp add:placeNewObject_def2) apply (wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap2 unless_doMachineOp_psp_no_overlap[simplified] | simp add: placeNewObject_def2 word_shiftl_add_distrib field_simps)+ apply (simp add:add.assoc[symmetric]) apply (wp createObjects'_pspace_no_overlap2 [where n =0 and sz = sz,simplified]) apply clarsimp apply (frule(1) range_cover_no_0[where p = n]) apply simp apply (frule pspace_no_overlap'_le2) apply (rule range_cover_compare_offset) apply simp+ apply (clarsimp simp:word_shiftl_add_distrib ,simp add:field_simps) apply (clarsimp simp:add.assoc[symmetric]) apply (rule range_cover_tail_mask[where n =0,simplified]) apply (drule range_cover_offset[rotated,where p = n]) apply simp apply (clarsimp simp:shiftl_t2n field_simps) apply (metis numeral_2_eq_2) apply (simp add:shiftl_t2n field_simps) apply (frule range_cover_offset[rotated,where p = n]) apply simp+ apply (auto simp: word_shiftl_add_distrib field_simps shiftl_t2n elim: range_cover_le, auto simp add: APIType_capBits_def fromAPIType_def objBits_def dest!: to_from_apiTypeD) done lemma createObject_pspace_aligned_distinct': "\pspace_aligned' and K (is_aligned ptr (APIType_capBits ty us)) and pspace_distinct' and pspace_no_overlap' ptr (APIType_capBits ty us) and K (ty = APIObjectType apiobject_type.CapTableObject \ us < 28)\ createObject ty ptr us d \\xa s. pspace_aligned' s \ pspace_distinct' s\" apply (rule hoare_pre) apply (wp placeNewObject_pspace_aligned' hoare_unless_wp placeNewObject_pspace_distinct' | simp add:ARM_H.createObject_def Retype_H.createObject_def objBits_simps curDomain_def placeNewDataObject_def split del: if_split | wpc | intro conjI impI)+ apply (auto simp:APIType_capBits_def pdBits_def objBits_simps pageBits_def word_bits_def archObjSize_def ptBits_def ARM_H.toAPIType_def split:ARM_H.object_type.splits apiobject_type.splits) done lemma APIType_capBits[simp]: "Types_H.getObjectSize a b = APIType_capBits a b" apply (case_tac a) apply (clarsimp simp:getObjectSize_def APIType_capBits_def ARM_H.getObjectSize_def split:apiobject_type.splits simp: apiGetObjectSize_def tcbBlockSizeBits_def objBits_def objBitsKO_def pdBits_def epSizeBits_def ntfnSizeBits_def cteSizeBits_def ptBits_def pageBits_def)+ done lemma createNewObjects_Cons: assumes dlength: "length dest < 2 ^ word_bits" shows "createNewObjects ty src (dest @ [lt]) ptr us d = do createNewObjects ty src dest ptr us d; (RetypeDecls_H.createObject ty ((of_nat (length dest) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src lt) od" proof - from dlength have expand:"dest\[] \ [(0::word32) .e. of_nat (length dest)] = [0.e.of_nat (length dest - 1)] @ [of_nat (length dest)]" apply (cases dest) apply clarsimp+ apply (rule upto_enum_inc_1) apply (rule word_of_nat_less) apply (simp add: word_bits_conv minus_one_norm) done have length:"\length dest < 2 ^ word_bits;dest \ []\ \ length [(0::word32) .e. of_nat (length dest - 1)] = length dest" proof (induct dest) case Nil thus ?case by simp next case (Cons x xs) thus ?case by (simp add:unat_of_nat32) qed show ?thesis using dlength apply (case_tac "dest = []") apply (simp add: zipWithM_x_def createNewObjects_def sequence_x_def zipWith_def) apply (clarsimp simp:createNewObjects_def) apply (subst expand) apply simp apply (subst zipWithM_x_append1) apply (rule length) apply (simp add:field_simps)+ done qed lemma updateNewFreeIndex_cteCaps_of[wp]: "\\s. P (cteCaps_of s)\ updateNewFreeIndex slot \\rv s. P (cteCaps_of s)\" by (simp add: cteCaps_of_def, wp) lemma insertNewCap_wps[wp]: "\pspace_aligned'\ insertNewCap parent slot cap \\rv. pspace_aligned'\" "\pspace_distinct'\ insertNewCap parent slot cap \\rv. pspace_distinct'\" "\\s. P ((cteCaps_of s)(slot \ cap))\ insertNewCap parent slot cap \\rv s. P (cteCaps_of s)\" apply (simp_all add: insertNewCap_def) apply (wp hoare_drop_imps | simp add: o_def)+ apply (fastforce elim!: rsubst[where P=P]) done crunch typ_at'[wp]: insertNewCap "\s. P (typ_at' T p s)" (wp: crunch_wps) lemma createNewObjects_pspace_no_overlap': "\pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and K (range_cover ptr sz (Types_H.getObjectSize ty us) (Suc (length dests))) and K (ptr \ 0) and K (ty = APIObjectType apiobject_type.CapTableObject \ us < 28)\ createNewObjects ty src dests ptr us d \\rv s. pspace_aligned' s \ pspace_distinct' s \ pspace_no_overlap' ((of_nat (length dests) << APIType_capBits ty us) + ptr) sz s\" apply (rule hoare_gen_asm)+ proof (induct rule:rev_induct ) case Nil show ?case by (simp add:createNewObjects_def zipWithM_x_mapM mapM_Nil | wp)+ next case (snoc dest dests) have rc:"range_cover ptr sz (Types_H.getObjectSize ty us) (Suc (length dests))" apply (rule range_cover_le) apply (rule snoc) apply simp done show ?case using rc apply (subst createNewObjects_Cons) apply (drule range_cover.weak) apply (simp add: word_bits_def) apply (wp pspace_no_overlap'_lift) apply (simp add: conj_comms) apply (rule hoare_vcg_conj_lift) apply (rule hoare_post_imp[OF _ createObject_pspace_aligned_distinct']) apply simp apply (rule hoare_vcg_conj_lift) apply (rule hoare_post_imp[OF _ createObject_pspace_aligned_distinct']) apply simp apply (simp add:field_simps) apply (wp createObject_pspace_no_overlap') apply (clarsimp simp: conj_comms) apply (rule hoare_pre) apply (rule hoare_vcg_conj_lift) apply (rule hoare_post_imp[OF _ snoc.hyps]) apply (simp add:snoc)+ apply (rule hoare_vcg_conj_lift) apply (rule hoare_post_imp[OF _ snoc.hyps]) apply (simp add:snoc)+ apply wp apply (simp add: conj_comms field_simps) apply (rule hoare_post_imp) apply (erule context_conjI) apply (intro conjI) apply (rule aligned_add_aligned[OF range_cover.aligned is_aligned_shiftl_self]) apply simp apply simp apply simp apply (erule pspace_no_overlap'_le) apply (simp add: range_cover.sz[where 'a=32, folded word_bits_def])+ apply (rule hoare_post_imp[OF _ snoc.hyps]) apply (simp add:field_simps snoc)+ using snoc apply simp done qed end end