(* * 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) *) (* CSpace refinement *) theory CSpace_R imports CSpace1_R begin lemma setCTE_pred_tcb_at': "\pred_tcb_at' proj P t\ setCTE c cte \\rv. pred_tcb_at' proj P t\" unfolding pred_tcb_at'_def setCTE_def apply (rule setObject_cte_obj_at_tcb') apply (simp add: tcb_to_itcb'_def)+ done locale mdb_move = mdb_ptr m _ _ src src_cap src_node for m src src_cap src_node + fixes dest cap' fixes old_dest_node assumes dest: "m dest = Some (CTE NullCap old_dest_node)" assumes prev: "mdbPrev old_dest_node = 0" assumes nxt: "mdbNext old_dest_node = 0" assumes parency: "weak_derived' src_cap cap'" assumes not_null: "src_cap \ NullCap" assumes neq: "src \ dest" fixes n defines "n \ modify_map (modify_map (modify_map (modify_map (modify_map m dest (cteCap_update (\_. cap'))) src (cteCap_update (\_. NullCap))) dest (cteMDBNode_update (\m. src_node))) src (cteMDBNode_update (\m. nullMDBNode))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\_. dest)))" fixes m' defines "m' \ modify_map n (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\_. dest)))" begin lemmas src = m_p lemma [intro?]: shows src_0: "src \ 0" and dest_0: "dest \ 0" using no_0 src dest by (auto simp: no_0_def) lemma src_prev: "mdbPrev src_node \ dest" proof (cases "mdbPrev src_node = 0") case True thus ?thesis using dest_0 by simp next case False with src dlist obtain cte' where "m (mdbPrev src_node) = Some cte'" "mdbNext (cteMDBNode cte') = src" by (auto elim: valid_dlistE) with dest nxt src_0 show ?thesis apply - apply (rule notI) apply hypsubst apply simp done qed lemma src_neq_next: "src \ mdbNext src_node" by simp lemma src_neq_prev: "src \ mdbPrev src_node" by simp lemmas src_neq_next2 = src_neq_next [symmetric] lemmas src_neq_prev2 = src_neq_prev [symmetric] lemma n: "n = modify_map (m(dest \ CTE cap' src_node, src \ CTE capability.NullCap nullMDBNode)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\_. dest)))" using neq src dest no_0 by (simp add: n_def modify_map_apply) lemma dest_no_parent [iff]: "m \ dest \ x = False" using dest nxt by (auto dest: subtree_next_0) lemma dest_no_child [iff]: "m \ x \ dest = False" using dest prev by (auto dest: subtree_prev_0) lemma src_no_parent [iff]: "n \ src \ x = False" apply clarsimp apply (erule subtree_next_0) apply (auto simp add: n modify_map_def nullPointer_def) done lemma no_0_n: "no_0 n" by (simp add: n_def no_0) lemma no_0': "no_0 m'" by (simp add: m'_def no_0_n) lemma next_neq_dest [simp]: "mdbNext src_node \ dest" using dlist src dest prev dest_0 no_0 by (fastforce simp add: valid_dlist_def no_0_def Let_def) lemma prev_neq_dest [simp]: "mdbPrev src_node \ dest" using dlist src dest nxt dest_0 no_0 by (fastforce simp add: valid_dlist_def no_0_def Let_def) lemmas next_neq_dest2 [simp] = next_neq_dest [symmetric] lemmas prev_neq_dest2 [simp] = prev_neq_dest [symmetric] lemma prev_next_0: "(mdbPrev src_node = mdbNext src_node) = (mdbPrev src_node = 0 \ mdbNext src_node = 0)" proof - { assume "mdbPrev src_node = mdbNext src_node" moreover assume "mdbNext src_node \ 0" ultimately obtain cte where "m (mdbNext src_node) = Some cte" "mdbNext (cteMDBNode cte) = src" using src dlist by (fastforce simp add: valid_dlist_def Let_def) hence "m \ src \\<^sup>+ src" using src apply - apply (rule trancl_trans) apply (rule r_into_trancl) apply (simp add: next_unfold') apply (rule r_into_trancl) apply (simp add: next_unfold') done with no_loops have False by (simp add: no_loops_def) } thus ?thesis by auto qed lemma next_prev_0: "(mdbNext src_node = mdbPrev src_node) = (mdbPrev src_node = 0 \ mdbNext src_node = 0)" by auto lemma dlist': "valid_dlist m'" using src dest prev neq nxt dlist no_0 apply (simp add: m'_def n no_0_def) apply (simp add: valid_dlist_def Let_def) apply clarsimp apply (case_tac cte) apply (rename_tac cap node) apply (rule conjI) apply (clarsimp simp: modify_map_def nullPointer_def split: split_if_asm) apply (case_tac z) apply fastforce apply (case_tac z) apply (rename_tac capability mdbnode) apply clarsimp apply (rule conjI) apply fastforce apply clarsimp apply (rule conjI, fastforce) apply clarsimp apply (rule conjI) apply clarsimp apply (subgoal_tac "mdbNext mdbnode = mdbPrev src_node") prefer 2 apply fastforce apply (subgoal_tac "mdbNext mdbnode = src") prefer 2 apply fastforce apply fastforce apply clarsimp apply (rule conjI) apply clarsimp apply (frule_tac x=src in spec, erule allE, erule (1) impE) apply fastforce subgoal by fastforce subgoal by fastforce apply (rule conjI, clarsimp) apply fastforce apply (clarsimp, rule conjI, fastforce) apply (clarsimp, rule conjI) apply clarsimp apply (frule_tac x=src in spec, erule allE, erule (1) impE) subgoal by fastforce subgoal by fastforce apply (clarsimp simp: modify_map_def nullPointer_def split: split_if_asm) apply (case_tac z) apply (clarsimp, rule conjI, fastforce) apply (clarsimp, rule conjI, fastforce) apply (clarsimp, rule conjI) apply clarsimp apply (frule_tac x=src in spec, erule allE, erule (1) impE) subgoal by fastforce apply (clarsimp, rule conjI) apply clarsimp apply (frule_tac x=src in spec, erule allE, erule (1) impE) subgoal by fastforce subgoal by fastforce apply (case_tac z) subgoal by fastforce subgoal by fastforce apply (rule conjI) apply (clarsimp simp: next_prev_0) apply fastforce apply clarsimp apply (rule conjI, fastforce) apply (clarsimp, rule conjI) apply clarsimp apply (frule_tac x=src in spec, erule allE, erule (1) impE) subgoal by fastforce apply (clarsimp, rule conjI) apply clarsimp apply (frule_tac x=src in spec, erule allE, erule (1) impE) subgoal by fastforce subgoal by fastforce done lemma src_no_child [iff]: "n \ x \ src = False" proof - from src_neq_next have "m' src = Some (CTE capability.NullCap nullMDBNode)" by (simp add: m'_def n modify_map_def) hence "m' \ x \ src = False" using dlist' no_0' by (auto elim!: subtree_prev_0 simp: nullPointer_def) thus ?thesis by (simp add: m'_def) qed lemma [iff]: "m \ dest parentOf c = False" using dest by (simp add: parentOf_def) lemma [iff]: "mdbNext src_node \ dest" proof assume "mdbNext src_node = dest" moreover have "dest \ 0" .. ultimately have "mdbPrev old_dest_node = src" using src dest dlist by (fastforce elim: valid_dlistEn) with prev show False by (simp add: src_0) qed lemmas no_loops_simps [simp] = no_loops_direct_simp [OF no_loops] no_loops_trancl_simp [OF no_loops] lemma dest_source [iff]: "(m \ dest \ x) = (x = 0)" using dest nxt by (simp add: next_unfold') lemma dest_no_target [iff]: "m \ p \ dest = False" using dlist no_0 prev dest by (fastforce simp: valid_dlist_def Let_def no_0_def next_unfold') lemma no_src_subtree_m_n: assumes no_src: "\ m \ p \ src" "p \ src" assumes px: "m \ p \ x" assumes xs: "x \ src" shows "n \ p \ x" using px xs proof induct case (direct_parent c) thus ?case using neq no_src no_loops apply - apply (rule subtree.direct_parent) apply (clarsimp simp add: n mdb_next_update simp del: fun_upd_apply) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None) apply simp apply (clarsimp simp add: mdb_next_update simp del: fun_upd_apply) apply (subst modify_map_apply) apply simp apply (clarsimp simp add: mdb_next_update simp del: fun_upd_apply) apply (rule conjI) apply clarsimp apply (clarsimp) apply (drule prev_leadstoD) apply (rule src) apply (rule dlist) apply (rule no_0) apply simp apply assumption apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None) apply simp apply (clarsimp simp add: parentOf_def n) apply (rule conjI) apply clarsimp apply (fastforce simp add: parentOf_def n) apply (subst modify_map_apply) apply simp apply (fastforce simp add: parentOf_def n) done next case (trans_parent c c') thus ?case using no_src apply (cases "c = src") apply simp apply clarsimp apply (erule subtree.trans_parent) apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None) apply simp apply (clarsimp simp add: n mdb_next_update) apply (subst modify_map_apply) apply simp apply (clarsimp simp add: n mdb_next_update) apply (rule conjI, fastforce) apply clarsimp apply (drule prev_leadstoD) apply (rule src) apply (rule dlist) apply (rule no_0) apply simp apply assumption apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None) apply simp apply (clarsimp simp: parentOf_def n) apply (rule conjI) apply clarsimp apply (clarsimp simp: dest) apply (subst modify_map_apply) apply simp apply (fastforce simp: parentOf_def n) done qed lemma capMaster_isReply_eq: "capMasterCap c = capMasterCap c' \ isReplyCap c = isReplyCap c'" by (clarsimp simp: capMasterCap_def isCap_simps split: capability.split_asm) lemma parent_preserved: "isMDBParentOf cte' (CTE cap' src_node) = isMDBParentOf cte' (CTE src_cap src_node)" using parency unfolding weak_derived'_def apply (cases cte') apply (simp add: isMDBParentOf_CTE sameRegionAs_def2) done lemma children_preserved: "isMDBParentOf (CTE cap' src_node) cte' = isMDBParentOf (CTE src_cap src_node) cte'" using parency unfolding weak_derived'_def apply (cases cte') apply (simp add: isMDBParentOf_CTE sameRegionAs_def2) done lemma no_src_subtree_n_m: assumes no_src: "\ m \ p \ src" "p \ src" "p \ dest" assumes px: "n \ p \ x" shows "m \ p \ x" using px proof induct case (direct_parent c) thus ?case using neq no_src no_loops apply - apply (case_tac "c=dest") apply (cases "m (mdbPrev src_node)") apply (unfold n)[1] apply (subst (asm) modify_map_None, simp)+ apply (clarsimp simp: mdb_next_update) apply (rename_tac cte') apply clarsimp apply (subgoal_tac "p = mdbPrev src_node") prefer 2 apply (simp add: n) apply (subst (asm) modify_map_apply, simp) apply (clarsimp simp:_mdb_next_update split: split_if_asm) apply clarsimp apply (simp add: n) apply (subst (asm) modify_map_apply, simp)+ apply (insert dest)[1] apply (clarsimp simp add: parentOf_def mdb_next_unfold) apply (subgoal_tac "m \ mdbPrev src_node \ src") apply simp apply (rule subtree.direct_parent) apply (rule prev_leadstoI) apply (rule src) apply (insert no_0, clarsimp simp: no_0_def)[1] apply (rule dlist) apply (rule src_0) apply (simp add: parentOf_def src parent_preserved) apply (rule subtree.direct_parent) apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst (asm) modify_map_None, simp)+ apply (simp add: mdb_next_update) apply (subst (asm) modify_map_apply, simp)+ apply (simp add: mdb_next_update split: split_if_asm) apply assumption apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst (asm) modify_map_None, simp)+ apply (clarsimp simp add: parentOf_def split: split_if_asm) apply (subst (asm) modify_map_apply, simp)+ apply (clarsimp simp add: parentOf_def split: split_if_asm) done next case (trans_parent c c') thus ?case using neq no_src apply - apply (case_tac "c' = dest") apply clarsimp apply (subgoal_tac "c = mdbPrev src_node") prefer 2 apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst (asm) modify_map_None, simp)+ apply (clarsimp simp: mdb_next_update split: split_if_asm) apply (subst (asm) modify_map_apply, simp)+ apply (clarsimp simp: mdb_next_update split: split_if_asm) apply clarsimp apply (cases "m (mdbPrev src_node)") apply (unfold n)[1] apply (subst (asm) modify_map_None, simp)+ apply (clarsimp simp: mdb_next_update) apply (subgoal_tac "m \ p \ src") apply simp apply (rule subtree.trans_parent, assumption) apply (rule prev_leadstoI) apply (rule src) apply (insert no_0, clarsimp simp: no_0_def)[1] apply (rule dlist) apply (rule src_0) apply (clarsimp simp: n) apply (subst (asm) modify_map_apply, simp)+ apply (clarsimp simp: parentOf_def src parent_preserved split: split_if_asm) apply (rule subtree.trans_parent, assumption) apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst (asm) modify_map_None, simp)+ apply (simp add: mdb_next_update split: split_if_asm) apply (subst (asm) modify_map_apply, simp)+ apply (simp add: mdb_next_update split: split_if_asm) apply assumption apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst (asm) modify_map_None, simp)+ apply (clarsimp simp: parentOf_def split: split_if_asm) apply (subst (asm) modify_map_apply, simp)+ apply (clarsimp simp: parentOf_def split: split_if_asm) done qed lemma subtree_m_n: assumes p_neq: "p \ dest" "p \ src" assumes px: "m \ p \ x" shows "if x = src then n \ p \ dest else n \ p \ x" using px proof induct case (direct_parent c) thus ?case using p_neq apply - apply simp apply (rule conjI) apply clarsimp apply (drule leadsto_is_prev) apply (rule src) apply (rule dlist) apply (rule no_0) apply (clarsimp simp: parentOf_def) apply (rule subtree.direct_parent) apply (simp add: n modify_map_apply mdb_next_update) apply (rule dest_0) apply (clarsimp simp: n modify_map_apply parentOf_def neq [symmetric] src parent_preserved) apply clarsimp apply (rule subtree.direct_parent) apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None, simp) apply (simp add: mdb_next_update) apply (subst modify_map_apply, simp) apply (clarsimp simp: mdb_next_update) apply (drule prev_leadstoD) apply (rule src) apply (rule dlist) apply (rule no_0) apply simp apply assumption apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None, simp) apply (clarsimp simp add: parentOf_def) apply (subst modify_map_apply, simp) apply (clarsimp simp add: parentOf_def) apply fastforce done next case (trans_parent c c') thus ?case using p_neq apply - apply (clarsimp split: split_if_asm) apply (erule subtree.trans_parent) apply (clarsimp simp: next_unfold' src n) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None, simp) apply (clarsimp simp add: neq [symmetric] src split: option.splits) apply (subst modify_map_apply, simp) apply (clarsimp simp add: neq [symmetric] src split: option.splits) apply assumption apply (clarsimp simp: mdb_next_unfold src n) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None, simp) apply (simp add: parentOf_def) apply (subst modify_map_apply, simp) apply (fastforce simp add: parentOf_def) apply (rule conjI) apply clarsimp apply (cases "m c", simp add: mdb_next_unfold) apply (drule leadsto_is_prev) apply (rule src) apply (rule dlist) apply (rule no_0) apply clarsimp apply (erule subtree.trans_parent) apply (simp add: n modify_map_apply mdb_next_update) apply (rule dest_0) apply (clarsimp simp: n modify_map_apply parentOf_def neq [symmetric] src) apply (rule conjI, clarsimp) apply (clarsimp simp: parent_preserved) apply clarsimp apply (erule subtree.trans_parent) apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None, simp) apply (clarsimp simp add: mdb_next_update) apply (subst modify_map_apply, simp) apply (clarsimp simp add: mdb_next_update) apply (rule conjI, clarsimp) apply clarsimp apply (drule prev_leadstoD, rule src, rule dlist, rule no_0) apply simp apply assumption apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None, simp) apply (clarsimp simp add: parentOf_def) apply (subst modify_map_apply, simp) apply (fastforce simp add: parentOf_def) done qed lemmas neq_sym [simp] = neq [symmetric] lemma sub_tree_loop [simp]: "m \ x \ x = False" by (clarsimp dest!: subtree_mdb_next) lemmas src_prev_loop [simp] = subtree_prev_loop [OF src no_loops dlist no_0] lemma subtree_src_dest: "m \ src \ x \ n \ dest \ x" apply (erule subtree.induct) apply (clarsimp simp: mdb_next_unfold src) apply (rule subtree.direct_parent) apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None, simp) apply (simp add: mdb_next_update) apply (subst modify_map_apply, simp) apply (simp add: mdb_next_update) apply assumption apply (simp add: n) apply (clarsimp simp add: modify_map_def parentOf_def src children_preserved) apply (subgoal_tac "c'' \ src") prefer 2 apply (drule (3) subtree.trans_parent) apply clarsimp apply (erule subtree.trans_parent) apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst modify_map_None, simp) apply (simp add: mdb_next_update) apply fastforce apply (subst modify_map_apply, simp) apply (simp add: mdb_next_update) apply fastforce apply assumption apply (fastforce simp: n modify_map_def parentOf_def src children_preserved) done lemma src_next [simp]: "m \ src \ mdbNext src_node" by (simp add: next_unfold' src) lemma dest_no_trancl_target [simp]: "m \ x \\<^sup>+ dest = False" by (clarsimp dest!: tranclD2) lemma m'_next: "\m' p = Some (CTE cte' node'); m p = Some (CTE cte node)\ \ mdbNext node' = (if p = src then 0 else if p = dest then mdbNext src_node else if mdbNext node = src then dest else mdbNext node)" apply(simp, intro conjI impI) apply(clarsimp simp: n m'_def modify_map_def split: split_if_asm) apply(clarsimp simp: n m'_def modify_map_def nullPointer_def) apply(subgoal_tac "mdbPrev src_node = p") prefer 2 apply(erule dlistEn) apply(simp) apply(case_tac "cte'a") apply(clarsimp simp: src) apply(clarsimp simp: n m'_def modify_map_def split: split_if_asm) apply(clarsimp simp: dest n m'_def modify_map_def) apply(clarsimp simp: n m'_def modify_map_def nullPointer_def) apply(clarsimp simp: n m'_def modify_map_def split: split_if_asm) apply(insert m_p no_0) apply(erule_tac p=src in dlistEp) apply(clarsimp simp: no_0_def) apply(clarsimp) done lemma mdb_next_from_dest: "n \ dest \\<^sup>+ x \ m \ src \\<^sup>+ x" apply (erule trancl_induct) apply (rule r_into_trancl) apply (simp add: n modify_map_def next_unfold' src) apply (cases "m (mdbPrev src_node)") apply (simp add: n) apply (subst (asm) modify_map_None, simp)+ apply (clarsimp simp: mdb_next_update split: split_if_asm) apply (fastforce intro: trancl_into_trancl) apply (simp add: n) apply (subst (asm) modify_map_apply, simp)+ apply (clarsimp simp: mdb_next_update split: split_if_asm) apply (subgoal_tac "m \ src \\<^sup>+ src") apply simp apply (erule trancl_into_trancl) apply (rule prev_leadstoI, rule src) apply (insert no_0)[1] apply (clarsimp simp add: no_0_def) apply (rule dlist) apply (fastforce intro: trancl_into_trancl) done lemma dest_loop: "n \ dest \ dest = False" apply clarsimp apply (drule subtree_mdb_next) apply (drule mdb_next_from_dest) apply simp done lemma subtree_dest_src: "n \ dest \ x \ m \ src \ x" apply (erule subtree.induct) apply (clarsimp simp: mdb_next_unfold src) apply (rule subtree.direct_parent) apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst (asm) modify_map_None, simp)+ apply (clarsimp simp add: mdb_next_update next_unfold src) apply (subst (asm) modify_map_apply, simp)+ apply (clarsimp simp add: mdb_next_update next_unfold src) apply assumption apply (simp add: n) apply (simp add: modify_map_def parentOf_def) apply (clarsimp simp: next_prev_0 src children_preserved) apply (subgoal_tac "c' \ dest") prefer 2 apply clarsimp apply (subgoal_tac "c'' \ dest") prefer 2 apply clarsimp apply (drule (3) trans_parent) apply (simp add: dest_loop) apply (subgoal_tac "c' \ mdbPrev src_node") prefer 2 apply clarsimp apply (erule subtree.trans_parent) apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst (asm) modify_map_None, simp)+ apply (simp add: mdb_next_update nullPointer_def split: split_if_asm) apply (subst (asm) modify_map_apply, simp)+ apply (simp add: mdb_next_update nullPointer_def split: split_if_asm) apply assumption apply (clarsimp simp add: n modify_map_def parentOf_def src children_preserved split: split_if_asm) done lemma subtree_n_m: assumes p_neq: "p \ dest" "p \ src" assumes px: "n \ p \ x" shows "if x = dest then m \ p \ src else m \ p \ x" using px proof induct case (direct_parent c) thus ?case using p_neq apply clarsimp apply (rule conjI) apply clarsimp apply (subgoal_tac "p = mdbPrev src_node") prefer 2 apply (drule mdb_next_modify_prev [where x="mdbNext src_node" and f="\_. dest", THEN iffD2]) apply (fold m'_def) apply (drule leadsto_is_prev) apply (fastforce simp: n m'_def modify_map_def) apply (rule dlist') apply (rule no_0') apply simp apply clarsimp apply (rule subtree.direct_parent) apply (rule prev_leadstoI) apply (rule src) apply (insert no_0)[1] apply (clarsimp simp add: next_unfold' n modify_map_def no_0_def split: split_if_asm) apply (rule dlist) apply (rule src_0) apply (clarsimp simp: parentOf_def n modify_map_def src parent_preserved) apply clarsimp apply (rule subtree.direct_parent) apply (simp add: n) apply (cases "m (mdbPrev src_node)") apply (subst (asm) modify_map_None, simp)+ apply (simp add: next_unfold' mdb_next_unfold) apply (subst (asm) modify_map_apply, simp)+ apply (simp add: mdb_next_update split: split_if_asm) apply assumption apply (simp add: n) apply (clarsimp simp add: parentOf_def modify_map_def split: split_if_asm) done next case (trans_parent c c') thus ?case using p_neq apply - apply (simp split: split_if_asm) apply clarsimp apply (subgoal_tac "c' = mdbNext src_node") prefer 2 apply (clarsimp simp add: mdb_next_unfold n modify_map_def) apply clarsimp apply (erule subtree.trans_parent) apply (simp add: mdb_next_unfold src) apply assumption apply (clarsimp simp add: parentOf_def modify_map_def n split: split_if_asm) apply (rule conjI) apply clarsimp apply (subgoal_tac "c = mdbPrev src_node") prefer 2 apply (drule mdb_next_modify_prev [where x="mdbNext src_node" and f="\_. dest", THEN iffD2]) apply (fold m'_def) apply (drule leadsto_is_prev) apply (fastforce simp: n m'_def modify_map_def) apply (rule dlist') apply (rule no_0') apply simp apply clarsimp apply (erule subtree.trans_parent) apply (rule prev_leadstoI) apply (rule src) apply (insert no_0)[1] apply (clarsimp simp: next_unfold' no_0_def n modify_map_def) apply (rule dlist) apply (rule src_0) apply (clarsimp simp: parentOf_def n modify_map_def src parent_preserved split: split_if_asm) apply clarsimp apply (erule subtree.trans_parent) apply (clarsimp simp add: n modify_map_def mdb_next_unfold nullPointer_def split: split_if_asm) apply assumption apply (clarsimp simp add: n modify_map_def parentOf_def split: split_if_asm) done qed lemma descendants: "descendants_of' p m' = (if p = src then {} else if p = dest then descendants_of' src m else descendants_of' p m - {src} \ (if src \ descendants_of' p m then {dest} else {}))" apply (rule set_eqI) apply (simp add: descendants_of'_def m'_def) apply (auto simp: subtree_m_n intro: subtree_src_dest subtree_dest_src no_src_subtree_n_m) apply (auto simp: subtree_n_m) done end context mdb_move_abs begin end context mdb_move begin lemma descendants_dest: "descendants_of' dest m = {}" by (simp add: descendants_of'_def) lemma dest_descendants: "dest \ descendants_of' x m" by (simp add: descendants_of'_def) end lemma updateCap_dynamic_duo: "\ (rv, s') \ fst (updateCap x cap s); pspace_aligned' s; pspace_distinct' s \ \ pspace_aligned' s' \ pspace_distinct' s'" unfolding updateCap_def apply (rule conjI) apply (erule use_valid | wp | assumption)+ done declare const_apply[simp] lemma next_slot_eq2: "\case n q of None \ next_slot p t' m' = x | Some q' \ next_slot p (t'' q') (m'' q') = x; case n q of None \ (t' = t \ m' = m) | Some q' \ t'' q' = t \ m'' q' = m\ \ next_slot p t m = x" apply(simp split: option.splits) done abbreviation "einvs \ (invs and valid_list and valid_sched)" lemma set_cap_not_quite_corres': assumes cr: "pspace_relations (ekheap (a)) (kheap s) (ksPSpace s')" "ekheap (s) = ekheap (a)" "cur_thread s = ksCurThread s'" "idle_thread s = ksIdleThread s'" "machine_state s = ksMachineState s'" "work_units_completed s = ksWorkUnitsCompleted s'" "domain_index s = ksDomScheduleIdx s'" "domain_list s = ksDomSchedule s'" "cur_domain s = ksCurDomain s'" "domain_time s = ksDomainTime s'" "(x,t') \ fst (updateCap p' c' s')" "valid_objs s" "pspace_aligned s" "pspace_distinct s" "cte_at p s" "pspace_aligned' s'" "pspace_distinct' s'" "interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s')" "(arch_state s, ksArchState s') \ arch_state_relation" assumes c: "cap_relation c c'" assumes p: "p' = cte_map p" shows "\t. ((),t) \ fst (set_cap c p s) \ pspace_relations (ekheap t) (kheap t) (ksPSpace t') \ cdt t = cdt s \ cdt_list t = cdt_list (s) \ ekheap t = ekheap (s) \ scheduler_action t = scheduler_action (s) \ ready_queues t = ready_queues (s) \ is_original_cap t = is_original_cap s \ interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState t') \ (arch_state t, ksArchState t') \ arch_state_relation \ cur_thread t = ksCurThread t' \ idle_thread t = ksIdleThread t' \ machine_state t = ksMachineState t' \ work_units_completed t = ksWorkUnitsCompleted t' \ domain_index t = ksDomScheduleIdx t' \ domain_list t = ksDomSchedule t' \ cur_domain t = ksCurDomain t' \ domain_time t = ksDomainTime t'" apply (rule set_cap_not_quite_corres) using cr apply (fastforce simp: c p pspace_relations_def)+ done lemma cap_move_corres: assumes cr: "cap_relation cap cap'" notes trans_state_update'[symmetric,simp] shows "corres dc (einvs and cte_at ptr and cte_wp_at (\c. c = cap.NullCap) ptr' and valid_cap cap and tcb_cap_valid cap ptr' and K (ptr \ ptr')) (invs' and cte_wp_at' (\c. weak_derived' cap' (cteCap c) \ cteCap c \ NullCap) (cte_map ptr) and cte_wp_at' (\c. cteCap c = NullCap) (cte_map ptr')) (cap_move cap ptr ptr') (cteMove cap' (cte_map ptr) (cte_map ptr'))" (is "corres _ ?P ?P' _ _") apply (simp add: cap_move_def cteMove_def const_def) apply (rule corres_symb_exec_r) defer apply (rule getCTE_sp) apply wp apply (rule no_fail_pre, wp) apply (clarsimp simp add: cte_wp_at_ctes_of) apply (rule corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of) apply (rule corres_assert_assume) prefer 2 apply clarsimp apply (drule invs_mdb') apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def) apply (case_tac oldCTE) apply (clarsimp simp: valid_nullcaps_def initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) apply (clarsimp simp: nullPointer_def) apply (rule corres_symb_exec_r) defer apply (rule getCTE_sp) apply wp apply (rule no_fail_pre, wp) apply (clarsimp simp add: cte_wp_at_ctes_of) apply (rule corres_no_failI) apply (rule no_fail_pre, wp hoare_weak_lift_imp) apply (clarsimp simp add: cte_wp_at_ctes_of) apply (drule invs_mdb') apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def) apply (rule conjI) apply clarsimp apply (erule (2) valid_dlistEp, simp) apply clarsimp apply (erule (2) valid_dlistEn, simp) apply (clarsimp simp: in_monad state_relation_def) apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac oldCTE) apply (rename_tac x old_dest_node) apply (case_tac cte) apply (rename_tac src_cap src_node) apply clarsimp apply (subgoal_tac "\c. caps_of_state a ptr = Some c") prefer 2 apply (clarsimp simp: cte_wp_at_caps_of_state) apply clarsimp apply (subgoal_tac "cap_relation c src_cap") prefer 2 apply (drule caps_of_state_cteD) apply (drule (1) pspace_relation_ctes_ofI) apply fastforce apply fastforce apply fastforce apply (drule (1) pspace_relationsD) apply (drule_tac p=ptr' in set_cap_not_quite_corres, assumption+) apply fastforce apply fastforce apply fastforce apply (erule cte_wp_at_weakenE, rule TrueI) apply fastforce apply fastforce apply assumption apply fastforce apply (rule cr) apply (rule refl) apply (clarsimp simp: split_def) apply (rule bind_execI, assumption) apply (drule_tac p=ptr and c="cap.NullCap" in set_cap_not_quite_corres') apply assumption+ apply (frule use_valid [OF _ set_cap_valid_objs]) apply fastforce apply assumption apply (frule use_valid [OF _ set_cap_aligned]) apply fastforce apply assumption apply (frule use_valid [OF _ set_cap_distinct]) apply fastforce apply assumption apply (frule use_valid [OF _ set_cap_cte_at]) prefer 2 apply assumption apply assumption apply (drule updateCap_stuff) apply (elim conjE mp, fastforce) apply (drule updateCap_stuff) apply (elim conjE mp, fastforce) apply assumption apply simp apply simp apply (rule refl) apply clarsimp apply (rule bind_execI, assumption) apply(subgoal_tac "mdb_move_abs ptr ptr' (cdt a) a") apply (frule mdb_move_abs'.intro) prefer 2 apply(rule mdb_move_abs.intro) apply(clarsimp) apply(fastforce elim!: cte_wp_at_weakenE) apply(simp) apply(simp) apply (clarsimp simp: exec_gets exec_get exec_put set_cdt_def set_original_def bind_assoc modify_def |(rule bind_execI[where f="cap_move_ext x y z x'" for x y z x'], clarsimp simp: mdb_move_abs'.cap_move_ext_det_def2 update_cdt_list_def set_cdt_list_def put_def) | rule refl )+ apply (clarsimp simp: put_def) apply (clarsimp simp: invs'_def valid_state'_def) apply (frule updateCap_dynamic_duo, fastforce, fastforce) apply (frule(2) updateCap_dynamic_duo [OF _ conjunct1 conjunct2]) apply (subgoal_tac "no_0 (ctes_of b)") prefer 2 apply fastforce apply (frule(1) use_valid [OF _ updateCap_no_0]) apply (frule(2) use_valid [OF _ updateCap_no_0, OF _ use_valid [OF _ updateCap_no_0]]) apply (elim conjE) apply (drule (5) updateMDB_the_lot', elim conjE) apply (drule (4) updateMDB_the_lot, elim conjE) apply (drule (4) updateMDB_the_lot, elim conjE) apply (drule (4) updateMDB_the_lot, elim conjE) apply (drule updateCap_stuff, elim conjE, erule (1) impE) apply (drule updateCap_stuff, clarsimp) apply (subgoal_tac "pspace_distinct' b \ pspace_aligned' b") prefer 2 subgoal by fastforce apply (thin_tac "ctes_of t = s" for t s)+ apply (thin_tac "ksMachineState t = p" for t p)+ apply (thin_tac "ksCurThread t = p" for t p)+ apply (thin_tac "ksIdleThread t = p" for t p)+ apply (thin_tac "ksReadyQueues t = p" for t p)+ apply (thin_tac "ksSchedulerAction t = p" for t p)+ apply (subgoal_tac "\p. cte_at p ta = cte_at p a") prefer 2 apply (simp add: set_cap_cte_eq) apply (clarsimp simp add: swp_def cte_wp_at_ctes_of simp del: split_paired_All) apply (subgoal_tac "cte_at ptr' a") prefer 2 apply (erule cte_wp_at_weakenE, rule TrueI) apply (subgoal_tac "cte_map ptr \ cte_map ptr'") prefer 2 apply (erule (2) cte_map_inj) apply fastforce apply fastforce apply fastforce apply (clarsimp simp: pspace_relations_def) apply (rule conjI) apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv) apply (subst conj_assoc[symmetric]) apply (rule conjI) defer apply (drule set_cap_caps_of_state_monad)+ apply (simp add: modify_map_mdb_cap) apply (simp add: modify_map_apply) apply (clarsimp simp add: revokable_relation_def simp del: fun_upd_apply) apply simp apply (rule conjI) apply clarsimp apply (erule_tac x="fst ptr" in allE) apply (erule_tac x="snd ptr" in allE) apply simp apply (erule impE) subgoal by (clarsimp simp: cte_wp_at_caps_of_state null_filter_def split: split_if_asm) apply simp apply clarsimp apply (subgoal_tac "null_filter (caps_of_state a) (aa,bb) \ None") prefer 2 subgoal by (clarsimp simp: null_filter_def split: if_splits) apply clarsimp apply (subgoal_tac "cte_at (aa,bb) a") prefer 2 apply (drule null_filter_caps_of_stateD) apply (erule cte_wp_cte_at) apply (frule_tac p="(aa,bb)" and p'="ptr'" in cte_map_inj, assumption+) apply fastforce apply fastforce apply fastforce apply (clarsimp split: split_if_asm) apply (subgoal_tac "(aa,bb) \ ptr") apply (frule_tac p="(aa,bb)" and p'="ptr" in cte_map_inj, assumption+) apply fastforce apply fastforce apply fastforce apply clarsimp subgoal by (simp add: null_filter_def split: if_splits) apply (subgoal_tac "mdb_move (ctes_of b) (cte_map ptr) src_cap src_node (cte_map ptr') cap' old_dest_node") prefer 2 apply (rule mdb_move.intro) apply (rule mdb_ptr.intro) apply (rule vmdb.intro) apply (simp add: valid_pspace'_def valid_mdb'_def) apply (erule mdb_ptr_axioms.intro) apply (rule mdb_move_axioms.intro) apply assumption apply (simp add: nullPointer_def) apply (simp add: nullPointer_def) apply (erule weak_derived_sym') apply clarsimp apply assumption apply (rule conjI) apply (simp (no_asm) add: cdt_relation_def) apply clarsimp apply (subst mdb_move.descendants, assumption) apply (subst mdb_move_abs.descendants[simplified fun_upd_apply]) apply (rule mdb_move_abs.intro) apply fastforce apply (fastforce elim!: cte_wp_at_weakenE) apply simp apply simp apply (case_tac "(aa,bb) = ptr", simp) apply (subgoal_tac "cte_map (aa,bb) \ cte_map ptr") prefer 2 apply (erule (2) cte_map_inj, fastforce, fastforce, fastforce) apply (case_tac "(aa,bb) = ptr'") apply (simp add: cdt_relation_def del: split_paired_All) apply (subgoal_tac "cte_map (aa,bb) \ cte_map ptr'") prefer 2 apply (erule (2) cte_map_inj, fastforce, fastforce, fastforce) apply (simp only: if_False) apply simp apply (subgoal_tac "descendants_of' (cte_map (aa, bb)) (ctes_of b) = cte_map ` descendants_of (aa, bb) (cdt a)") prefer 2 apply (simp add: cdt_relation_def del: split_paired_All) apply simp apply (rule conjI) apply clarsimp apply (subst inj_on_image_set_diff15) apply (rule inj_on_descendants_cte_map) apply fastforce apply fastforce apply fastforce apply fastforce apply (rule subset_refl) apply simp apply simp apply clarsimp apply (drule (1) cte_map_inj_eq) apply (erule descendants_of_cte_at) apply fastforce apply fastforce apply fastforce apply fastforce subgoal by clarsimp apply(clarsimp simp: cdt_list_relation_def) apply(subst next_slot_eq2) apply(simp split: option.splits) apply(intro conjI impI) apply(rule mdb_move_abs'.next_slot_no_parent) apply(simp, fastforce, simp) apply(intro allI impI) apply(rule mdb_move_abs'.next_slot) apply(simp, fastforce, simp) apply(fastforce split: option.splits) apply(case_tac "ctes_of b (cte_map (aa, bb))") subgoal by (clarsimp simp: modify_map_def split: split_if_asm) apply(case_tac ab) apply(frule mdb_move.m'_next) apply(simp, fastforce) apply(case_tac "(aa, bb) = ptr") apply(simp) apply(case_tac "(aa, bb) = ptr'") apply(case_tac "next_slot ptr (cdt_list (a)) (cdt a)") subgoal by(simp) apply(simp) apply(erule_tac x="fst ptr" in allE) apply(erule_tac x="snd ptr" in allE) subgoal by(clarsimp split: split_if_asm) apply(frule invs_mdb, frule invs_valid_pspace) apply(frule finite_depth) apply simp apply(case_tac "next_slot (aa, bb) (cdt_list (a)) (cdt a) = Some ptr") apply(frule(3) cte_at_next_slot) apply(erule_tac x=aa in allE, erule_tac x=bb in allE) subgoal by (clarsimp simp: cte_map_inj_eq valid_pspace_def split: split_if_asm) apply(simp) apply(case_tac "next_slot (aa, bb) (cdt_list (a)) (cdt a)") subgoal by(simp) apply(frule(3) cte_at_next_slot) apply(frule(3) cte_at_next_slot') apply(erule_tac x=aa in allE, erule_tac x=bb in allE) by(clarsimp simp: cte_map_inj_eq valid_pspace_def split: split_if_asm) lemmas cur_tcb_lift = hoare_lift_Pf [where f = ksCurThread and P = tcb_at', folded cur_tcb'_def] lemma valid_bitmapQ_lift: assumes prq: "\P. \\s. P (ksReadyQueues s) \ f \\_ s. P (ksReadyQueues s)\" and prqL1: "\P. \\s. P (ksReadyQueuesL1Bitmap s)\ f \\_ s. P (ksReadyQueuesL1Bitmap s)\" and prqL2: "\P. \\s. P (ksReadyQueuesL2Bitmap s)\ f \\_ s. P (ksReadyQueuesL2Bitmap s)\" shows "\Invariants_H.valid_bitmapQ\ f \\_. Invariants_H.valid_bitmapQ\" unfolding valid_bitmapQ_def bitmapQ_def apply (wp hoare_vcg_all_lift) apply (rule hoare_pre) apply (wps prq prqL1 prqL2) apply (rule hoare_vcg_prop, assumption) done lemma bitmapQ_no_L1_orphans_lift: assumes prq: "\P. \\s. P (ksReadyQueues s) \ f \\_ s. P (ksReadyQueues s)\" and prqL1: "\P. \\s. P (ksReadyQueuesL1Bitmap s)\ f \\_ s. P (ksReadyQueuesL1Bitmap s)\" and prqL2: "\P. \\s. P (ksReadyQueuesL2Bitmap s)\ f \\_ s. P (ksReadyQueuesL2Bitmap s)\" shows "\ bitmapQ_no_L1_orphans \ f \\_. bitmapQ_no_L1_orphans \" unfolding valid_bitmapQ_def bitmapQ_def bitmapQ_no_L1_orphans_def apply (wp hoare_vcg_all_lift) apply (rule hoare_pre) apply (wps prq prqL1 prqL2) apply (rule hoare_vcg_prop, assumption) done lemma bitmapQ_no_L2_orphans_lift: assumes prq: "\P. \\s. P (ksReadyQueues s) \ f \\_ s. P (ksReadyQueues s)\" and prqL1: "\P. \\s. P (ksReadyQueuesL1Bitmap s)\ f \\_ s. P (ksReadyQueuesL1Bitmap s)\" and prqL2: "\P. \\s. P (ksReadyQueuesL2Bitmap s)\ f \\_ s. P (ksReadyQueuesL2Bitmap s)\" shows "\ bitmapQ_no_L2_orphans \ f \\_. bitmapQ_no_L2_orphans \" unfolding valid_bitmapQ_def bitmapQ_def bitmapQ_no_L2_orphans_def apply (wp hoare_vcg_all_lift) apply (rule hoare_pre) apply (wps prq prqL1 prqL2) apply (rule hoare_vcg_prop, assumption) done lemma valid_queues_lift_asm: assumes tat1: "\d p tcb. \obj_at' (inQ d p) tcb and Q \ f \\_. obj_at' (inQ d p) tcb\" and tat2: "\tcb. \st_tcb_at' runnable' tcb and Q \ f \\_. st_tcb_at' runnable' tcb\" and prq: "\P. \\s. P (ksReadyQueues s) \ f \\_ s. P (ksReadyQueues s)\" and prqL1: "\P. \\s. P (ksReadyQueuesL1Bitmap s)\ f \\_ s. P (ksReadyQueuesL1Bitmap s)\" and prqL2: "\P. \\s. P (ksReadyQueuesL2Bitmap s)\ f \\_ s. P (ksReadyQueuesL2Bitmap s)\" shows "\Invariants_H.valid_queues and Q\ f \\_. Invariants_H.valid_queues\" proof - have tat: "\d p tcb. \obj_at' (inQ d p) tcb and st_tcb_at' runnable' tcb and Q\ f \\_. obj_at' (inQ d p) tcb and st_tcb_at' runnable' tcb\" apply (rule hoare_chain [OF hoare_vcg_conj_lift [OF tat1 tat2]]) apply (fastforce)+ done have tat_combined: "\d p tcb. \obj_at' (inQ d p and runnable' \ tcbState) tcb and Q\ f \\_. obj_at' (inQ d p and runnable' \ tcbState) tcb\" apply (rule hoare_chain [OF tat]) apply (fastforce simp add: obj_at'_and pred_tcb_at'_def o_def)+ done show ?thesis unfolding valid_queues_def valid_queues_no_bitmap_def by (wp tat_combined prq prqL1 prqL2 valid_bitmapQ_lift bitmapQ_no_L2_orphans_lift bitmapQ_no_L1_orphans_lift hoare_vcg_all_lift hoare_vcg_conj_lift hoare_Ball_helper) simp_all qed lemmas valid_queues_lift = valid_queues_lift_asm[where Q="\_. True", simplified] lemma valid_queues_lift': assumes tat: "\d p tcb. \\s. \ obj_at' (inQ d p) tcb s\ f \\_ s. \ obj_at' (inQ d p) tcb s\" and prq: "\P. \\s. P (ksReadyQueues s)\ f \\_ s. P (ksReadyQueues s)\" shows "\valid_queues'\ f \\_. valid_queues'\" unfolding valid_queues'_def imp_conv_disj by (wp hoare_vcg_all_lift hoare_vcg_disj_lift tat prq) lemma setCTE_norq [wp]: "\\s. P (ksReadyQueues s)\ setCTE ptr cte \\r s. P (ksReadyQueues s) \" by (clarsimp simp: valid_def dest!: setCTE_pspace_only) lemma setCTE_norqL1 [wp]: "\\s. P (ksReadyQueuesL1Bitmap s)\ setCTE ptr cte \\r s. P (ksReadyQueuesL1Bitmap s) \" by (clarsimp simp: valid_def dest!: setCTE_pspace_only) lemma setCTE_norqL2 [wp]: "\\s. P (ksReadyQueuesL2Bitmap s)\ setCTE ptr cte \\r s. P (ksReadyQueuesL2Bitmap s) \" by (clarsimp simp: valid_def dest!: setCTE_pspace_only) crunch nosch[wp]: cteInsert "\s. P (ksSchedulerAction s)" (wp: updateObject_cte_inv hoare_drop_imps) crunch norq[wp]: cteInsert "\s. P (ksReadyQueues s)" (wp: updateObject_cte_inv hoare_drop_imps) crunch norqL1[wp]: cteInsert "\s. P (ksReadyQueuesL1Bitmap s)" (wp: updateObject_cte_inv hoare_drop_imps) crunch norqL2[wp]: cteInsert "\s. P (ksReadyQueuesL2Bitmap s)" (wp: updateObject_cte_inv hoare_drop_imps) crunch typ_at'[wp]: cteInsert "\s. P (typ_at' T p s)" (wp: hoare_drop_imps setCTE_typ_at') lemmas updateMDB_typ_ats [wp] = typ_at_lifts [OF updateMDB_typ_at'] lemmas updateCap_typ_ats [wp] = typ_at_lifts [OF updateCap_typ_at'] lemmas cteInsert_typ_ats [wp] = typ_at_lifts [OF cteInsert_typ_at'] lemma setObject_cte_ct: "\\s. P (ksCurThread s)\ setObject t (v::cte) \\rv s. P (ksCurThread s)\" by (clarsimp simp: valid_def setCTE_def[symmetric] dest!: setCTE_pspace_only) crunch ct[wp]: cteInsert "\s. P (ksCurThread s)" (wp: setObject_cte_ct hoare_drop_imps ignore: setObject) context mdb_insert begin lemma n_src_dest: "n \ src \ dest" by (simp add: n_direct_eq) lemma dest_chain_0 [simp, intro!]: "n \ dest \\<^sup>+ 0" using chain_n n_dest by (simp add: mdb_chain_0_def) blast lemma m_tranclD: "m \ p \\<^sup>+ p' \ p' \ dest \ (p = dest \ p' = 0) \ n \ p \\<^sup>+ p'" apply (erule trancl_induct) apply (rule context_conjI, clarsimp) apply (rule context_conjI, clarsimp) apply (cases "p = src") apply simp apply (rule trancl_trans) apply (rule r_into_trancl) apply (rule n_src_dest) apply (rule r_into_trancl) apply (simp add: n_direct_eq) apply (cases "p = dest", simp) apply (rule r_into_trancl) apply (simp add: n_direct_eq) apply clarsimp apply (rule context_conjI, clarsimp) apply (rule context_conjI, clarsimp simp: mdb_next_unfold) apply (case_tac "y = src") apply clarsimp apply (erule trancl_trans) apply (rule trancl_trans) apply (rule r_into_trancl) apply (rule n_src_dest) apply (rule r_into_trancl) apply (simp add: n_direct_eq) apply (case_tac "y = dest", simp) apply (erule trancl_trans) apply (rule r_into_trancl) apply (simp add: n_direct_eq) done lemma n_trancl_eq': "n \ p \\<^sup>+ p' = (if p' = dest then m \ p \\<^sup>* src else if p = dest then m \ src \\<^sup>+ p' else m \ p \\<^sup>+ p')" apply (rule iffI) apply (erule trancl_induct) apply (clarsimp simp: n_direct_eq) apply (fastforce split: split_if_asm) apply (clarsimp simp: n_direct_eq split: split_if_asm) apply fastforce apply fastforce apply (fastforce intro: trancl_trans) apply (fastforce intro: trancl_trans) apply (simp split: split_if_asm) apply (drule rtranclD) apply (erule disjE) apply (fastforce intro: n_src_dest) apply (clarsimp dest!: m_tranclD) apply (erule trancl_trans) apply (fastforce intro: n_src_dest) apply (drule m_tranclD, clarsimp) apply (drule tranclD) apply clarsimp apply (insert n_src_dest)[1] apply (drule (1) next_single_value) apply (clarsimp simp: rtrancl_eq_or_trancl) apply (drule m_tranclD) apply clarsimp done lemma n_trancl_eq: "n \ p \\<^sup>+ p' = (if p' = dest then p = src \ m \ p \\<^sup>+ src else if p = dest then m \ src \\<^sup>+ p' else m \ p \\<^sup>+ p')" by (auto simp add: n_trancl_eq' rtrancl_eq_or_trancl) lemma n_rtrancl_eq: "n \ p \\<^sup>* p' = (if p' = dest then p = dest \ p \ dest \ m \ p \\<^sup>* src else if p = dest then p' \ src \ m \ src \\<^sup>* p' else m \ p \\<^sup>* p')" by (auto simp: n_trancl_eq rtrancl_eq_or_trancl) lemma n_cap: "n p = Some (CTE cap node) \ \node'. if p = dest then cap = c' \ m p = Some (CTE dest_cap node') else m p = Some (CTE cap node')" by (simp add: n src dest new_src_def new_dest_def split: split_if_asm) lemma m_cap: "m p = Some (CTE cap node) \ \node'. if p = dest then cap = dest_cap \ n p = Some (CTE c' node') else n p = Some (CTE cap node')" apply (simp add: n new_src_def new_dest_def) apply (cases "p=dest") apply (auto simp: src dest) done lemma chunked_m: "mdb_chunked m" using valid by (simp add: valid_mdb_ctes_def) lemma derived_region1 [simp]: "badge_derived' c' src_cap \ sameRegionAs c' cap = sameRegionAs src_cap cap" by (clarsimp simp add: badge_derived'_def sameRegionAs_def2) lemma derived_region2 [simp]: "badge_derived' c' src_cap \ sameRegionAs cap c' = sameRegionAs cap src_cap" by (clarsimp simp add: badge_derived'_def sameRegionAs_def2) lemma chunked_n: assumes b: "badge_derived' c' src_cap" shows "mdb_chunked n" using chunked_m src b apply (clarsimp simp: mdb_chunked_def) apply (drule n_cap)+ apply clarsimp apply (simp split: split_if_asm) apply clarsimp apply (erule_tac x=src in allE) apply (erule_tac x=p' in allE) apply simp apply (case_tac "src=p'") apply (clarsimp simp: n_trancl_eq) apply (clarsimp simp: is_chunk_def n_trancl_eq n_rtrancl_eq n_dest new_dest_def) apply (drule (1) trancl_rtrancl_trancl) apply simp apply (clarsimp simp: n_trancl_eq) apply (rule conjI) apply (clarsimp simp: is_chunk_def n_trancl_eq n_rtrancl_eq) apply (erule_tac x=p'' in allE) apply clarsimp apply (drule_tac p=p'' in m_cap) apply (clarsimp split: split_if_asm) apply clarsimp apply (clarsimp simp: is_chunk_def n_trancl_eq n_rtrancl_eq n_dest new_dest_def) apply (rule conjI) apply clarsimp apply (erule_tac x=src in allE) apply simp apply clarsimp apply (erule_tac x=p'' in allE) apply clarsimp apply (drule_tac p=p'' in m_cap) apply (clarsimp split: split_if_asm) apply (clarsimp simp: n_trancl_eq) apply (case_tac "p=src") apply (clarsimp simp: is_chunk_def n_trancl_eq n_rtrancl_eq n_dest new_dest_def) apply (drule (1) trancl_rtrancl_trancl) apply simp apply simp apply (erule_tac x=p in allE) apply (erule_tac x=src in allE) apply clarsimp apply (rule conjI) apply clarsimp apply (clarsimp simp: is_chunk_def n_trancl_eq n_rtrancl_eq n_dest new_dest_def) apply (erule_tac x=p'' in allE) apply clarsimp apply (drule_tac p=p'' in m_cap) apply clarsimp apply clarsimp apply (clarsimp simp: is_chunk_def n_trancl_eq n_rtrancl_eq n_dest new_dest_def) apply (erule_tac x=p'' in allE) apply clarsimp apply (drule_tac p=p'' in m_cap) apply clarsimp apply (clarsimp simp: n_trancl_eq) apply (erule_tac x=p in allE) apply (erule_tac x=p' in allE) apply clarsimp apply (rule conjI) apply clarsimp apply (simp add: is_chunk_def n_trancl_eq n_rtrancl_eq n_dest new_dest_def) apply clarsimp apply (rule conjI) apply clarsimp apply (rule conjI) apply clarsimp apply (erule sameRegionAsE, simp_all add: sameRegionAs_def3)[1] apply blast apply blast apply (clarsimp simp: isCap_simps) apply fastforce apply clarsimp apply (erule_tac x=p'' in allE) apply clarsimp apply (drule_tac p=p'' in m_cap) apply clarsimp apply clarsimp apply (simp add: is_chunk_def n_trancl_eq n_rtrancl_eq n_dest new_dest_def) apply clarsimp apply (rule conjI) apply clarsimp apply (rule conjI) apply clarsimp apply (erule_tac x=p in allE, simp, erule(1) sameRegionAs_trans) apply fastforce apply clarsimp apply (erule_tac x=p'' in allE) apply clarsimp apply (drule_tac p=p'' in m_cap) apply clarsimp done end context mdb_insert_der begin lemma untyped_c': "untypedRange c' = untypedRange src_cap" "isUntypedCap c' = isUntypedCap src_cap" using partial_is_derived' apply - apply (case_tac "isUntypedCap src_cap") by (clarsimp simp:isCap_simps freeIndex_update_def is_derived'_def badge_derived'_def capMasterCap_def split:if_splits capability.splits)+ lemma capRange_c': "capRange c' = capRange src_cap" using partial_is_derived' untyped_c' apply - apply (case_tac "isUntypedCap src_cap") apply (clarsimp simp:untypedCapRange) apply (rule master_eqI, rule capRange_Master) apply simp apply (rule arg_cong) apply (auto simp:isCap_simps freeIndex_update_def is_derived'_def badge_derived'_def capMasterCap_def split:if_splits capability.splits) done lemma untyped_no_parent: "isUntypedCap src_cap \ \ m \ src \ p" using partial_is_derived' untyped_c' by (clarsimp simp: is_derived'_def isCap_simps freeIndex_update_def descendants_of'_def) end lemma (in mdb_insert) n_revocable: "n p = Some (CTE cap node) \ \node'. if p = dest then mdbRevocable node = revokable' src_cap c' else mdbRevocable node = mdbRevocable node' \ m p = Some (CTE cap node')" using src dest by (clarsimp simp: n new_src_def new_dest_def split: split_if_asm) lemma (in mdb_insert_der) irq_control_n: "irq_control n" using src dest partial_is_derived' apply (clarsimp simp: irq_control_def) apply (frule n_cap) apply (drule n_revocable) apply (clarsimp split: split_if_asm) apply (simp add: is_derived'_def isCap_simps) apply (frule irq_revocable, rule irq_control) apply clarsimp apply (drule n_cap) apply (clarsimp split: split_if_asm) apply (erule disjE) apply (clarsimp simp: is_derived'_def isCap_simps) apply (erule (1) irq_controlD, rule irq_control) done context mdb_insert_child begin lemma untyped_mdb_n: shows "untyped_mdb' n" using untyped_mdb apply (clarsimp simp add: untyped_mdb'_def descendants split del: split_if) apply (drule n_cap)+ apply (clarsimp split: split_if_asm) apply (erule disjE, clarsimp) apply (simp add: descendants_of'_def) apply (erule_tac x=p in allE) apply (erule_tac x=src in allE) apply (simp add: src untyped_c' capRange_c') apply (erule disjE) apply clarsimp apply (simp add: descendants_of'_def untyped_c') apply (erule_tac x=src in allE) apply (erule_tac x=p' in allE) apply (fastforce simp: src dest: untyped_no_parent) apply (case_tac "p=src", simp) apply simp done lemma parent_untyped_must_not_usable: "\ptr \ src; m ptr = Some (CTE ccap node'); untypedRange ccap = untypedRange src_cap; capAligned src_cap; isUntypedCap src_cap \ \ usableUntypedRange ccap = {}" using untyped_inc src apply (clarsimp simp:untyped_inc'_def) apply (erule_tac x = ptr in allE) apply (erule_tac x = src in allE) apply clarsimp apply (subgoal_tac "isUntypedCap ccap") apply clarsimp apply (drule_tac p = ptr in untyped_no_parent) apply (simp add:descendants_of'_def) apply (drule (1) aligned_untypedRange_non_empty) apply (case_tac ccap,simp_all add:isCap_simps) done lemma untyped_inc_n: "\capAligned src_cap;isUntypedCap src_cap \ usableUntypedRange src_cap = {}\ \ untyped_inc' n" using untyped_inc apply (clarsimp simp add: untyped_inc'_def descendants split del: split_if) apply (drule n_cap)+ apply (clarsimp split: split_if_asm) apply (case_tac "p=dest", simp) apply (simp add: descendants_of'_def untyped_c') apply (erule_tac x=p in allE) apply (erule_tac x=src in allE) apply (simp add: src) apply (frule_tac p=p in untyped_no_parent) apply clarsimp apply (erule disjE) apply clarsimp apply (case_tac "p = src") using src apply clarsimp apply (drule(4) parent_untyped_must_not_usable) apply simp apply (intro conjI) apply clarsimp apply clarsimp using src apply clarsimp apply clarsimp apply (case_tac "p=dest") apply (simp add: descendants_of'_def untyped_c') apply (erule_tac x=p' in allE) apply (erule_tac x=src in allE) apply (clarsimp simp:src) apply (frule_tac p=p' in untyped_no_parent) apply (case_tac "p' = src") apply (clarsimp simp:src) apply (elim disjE) apply (erule disjE[OF iffD1[OF subset_iff_psubset_eq]]) apply simp+ apply (erule disjE[OF iffD1[OF subset_iff_psubset_eq]]) apply simp+ apply (clarsimp simp:Int_ac) apply (erule_tac x=p' in allE) apply (erule_tac x=p in allE) apply (case_tac "p' = src") apply (clarsimp simp:src descendants_of'_def untyped_c') apply (elim disjE) apply (erule disjE[OF iffD1[OF subset_iff_psubset_eq]]) apply (simp,intro conjI,clarsimp+) apply (intro conjI) apply clarsimp+ apply (erule disjE[OF iffD1[OF subset_iff_psubset_eq]]) apply (simp,intro conjI,clarsimp+) apply (intro conjI) apply clarsimp+ apply (clarsimp simp:Int_ac,intro conjI,clarsimp+) apply (clarsimp simp:descendants_of'_def) apply (case_tac "p = src") apply simp apply (elim disjE) apply (erule disjE[OF iffD1[OF subset_iff_psubset_eq]]) apply (simp,intro conjI,clarsimp+) apply (intro conjI) apply clarsimp+ apply (erule disjE[OF iffD1[OF subset_iff_psubset_eq]]) apply clarsimp+ apply fastforce apply (clarsimp simp:Int_ac,intro conjI,clarsimp+) apply (intro conjI) apply (elim disjE) apply (simp add:Int_ac)+ apply clarsimp done end context mdb_insert_sib begin lemma untyped_mdb_n: shows "untyped_mdb' n" using untyped_mdb apply (clarsimp simp add: untyped_mdb'_def descendants split del: split_if) apply (drule n_cap)+ apply (clarsimp split: split_if_asm simp: descendants_of'_def capRange_c' untyped_c') apply (erule_tac x=src in allE) apply (erule_tac x=p' in allE) apply (fastforce simp: src dest: untyped_no_parent) apply (erule_tac x=p in allE) apply (erule_tac x=src in allE) apply (simp add: src) done lemma not_untyped: "capAligned c' \ \isUntypedCap src_cap" using no_child partial_is_derived' ut_rev src apply (clarsimp simp: ut_revocable'_def isMDBParentOf_CTE) apply (erule_tac x=src in allE) apply simp apply (clarsimp simp: is_derived'_def freeIndex_update_def isCap_simps capAligned_def badge_derived'_def) apply (clarsimp simp: sameRegionAs_def3 capMasterCap_def isCap_simps interval_empty is_aligned_no_overflow split:capability.splits) done lemma untyped_inc_n: assumes c': "capAligned c'" shows "untyped_inc' n" using untyped_inc not_untyped [OF c'] apply (clarsimp simp add: untyped_inc'_def descendants split del: split_if) apply (drule n_cap)+ apply (clarsimp split: split_if_asm) apply (simp add: descendants_of'_def untyped_c') apply (case_tac "p = dest") apply (clarsimp simp: untyped_c') apply simp apply (erule_tac x=p in allE) apply (erule_tac x=p' in allE) apply simp done end lemma trancl_prev_update: "modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \ x \\<^sup>+ y = m \ x \\<^sup>+ y" apply (rule iffI) apply (erule update_prev_next_trancl2) apply (erule update_prev_next_trancl) done lemma rtrancl_prev_update: "modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \ x \\<^sup>* y = m \ x \\<^sup>* y" by (simp add: trancl_prev_update rtrancl_eq_or_trancl) lemma mdb_chunked_prev_update: "mdb_chunked (modify_map m x (cteMDBNode_update (mdbPrev_update f))) = mdb_chunked m" apply (simp add: mdb_chunked_def trancl_prev_update rtrancl_prev_update is_chunk_def) apply (rule iffI) apply clarsimp apply (erule_tac x=p in allE) apply (erule_tac x=p' in allE) apply (erule_tac x=cap in allE) apply (simp add: modify_map_if split: split_if_asm) apply (erule impE, blast) apply (erule allE, erule impE, blast) apply clarsimp apply blast apply clarsimp apply (erule_tac x=p in allE) apply (erule_tac x=p' in allE) apply (erule_tac x=cap in allE) apply (simp add: modify_map_if split: split_if_asm) apply (erule impE, blast) apply clarsimp apply blast apply (erule allE, erule impE, blast) apply clarsimp apply blast apply clarsimp apply blast done lemma descendants_of_prev_update: "descendants_of' p (modify_map m x (cteMDBNode_update (mdbPrev_update f))) = descendants_of' p m" by (simp add: descendants_of'_def) lemma untyped_mdb_prev_update: "untyped_mdb' (modify_map m x (cteMDBNode_update (mdbPrev_update f))) = untyped_mdb' m" apply (simp add: untyped_mdb'_def descendants_of_prev_update) apply (rule iffI) apply clarsimp apply (erule_tac x=p in allE) apply (erule_tac x=p' in allE) apply (erule_tac x=c in allE) apply (simp add: modify_map_if split: split_if_asm) apply (erule impE, blast) apply (erule allE, erule impE, blast) apply clarsimp apply clarsimp apply (erule_tac x=p in allE) apply (erule_tac x=p' in allE) apply (erule_tac x=c in allE) apply (simp add: modify_map_if split: split_if_asm) apply clarsimp done lemma untyped_inc_prev_update: "untyped_inc' (modify_map m x (cteMDBNode_update (mdbPrev_update f))) = untyped_inc' m" apply (simp add: untyped_inc'_def descendants_of_prev_update) apply (rule iffI) apply clarsimp apply (erule_tac x=p in allE) apply (erule_tac x=p' in allE) apply (erule_tac x=c in allE) apply (simp add: modify_map_if split: split_if_asm) apply (erule impE, blast) apply (erule allE, erule impE, blast) apply clarsimp apply clarsimp apply (erule_tac x=p in allE) apply (erule_tac x=p' in allE) apply (erule_tac x=c in allE) apply (simp add: modify_map_if split: split_if_asm) apply clarsimp done lemma is_derived_badge_derived': "is_derived' m src cap cap' \ badge_derived' cap cap'" by (simp add: is_derived'_def) lemma cteInsert_mdb_chain_0: "\valid_mdb' and pspace_aligned' and pspace_distinct' and (\s. src \ dest) and (\s. cte_wp_at' (is_derived' (ctes_of s) src cap \ cteCap) src s)\ cteInsert cap src dest \\_ s. mdb_chain_0 (ctes_of s)\" apply (unfold cteInsert_def updateCap_def) apply (fold revokable'_fold) apply (simp add: valid_mdb'_def split del: split_if) apply (wp updateMDB_ctes_of_no_0 getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of simp del: fun_upd_apply) apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift setUntypedCapAsFull_ctes_of setUntypedCapAsFull_ctes_of_no_0 mdb_inv_preserve_modify_map setUntypedCapAsFull_mdb_chain_0 mdb_inv_preserve_fun_upd | simp del:fun_upd_apply)+ apply (wp getCTE_wp) apply (clarsimp simp:cte_wp_at_ctes_of simp del:fun_upd_apply) apply (subgoal_tac "src \ 0") prefer 2 apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (subgoal_tac "dest \ 0") prefer 2 apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (rule conjI) apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (case_tac cte) apply (rename_tac s_cap s_node) apply (case_tac x) apply (simp add: nullPointer_def) apply (subgoal_tac "mdb_insert (ctes_of s) src s_cap s_node dest NullCap node" for node) apply (drule mdb_insert.chain_n) apply (rule mdb_chain_0_modify_map_prev) apply (simp add:modify_map_apply) apply (clarsimp simp: valid_badges_def) apply unfold_locales apply (assumption|rule refl)+ apply (simp add: valid_mdb_ctes_def) apply (simp add: valid_mdb_ctes_def) apply assumption done lemma cteInsert_mdb_chunked: "\valid_mdb' and pspace_aligned' and pspace_distinct' and (\s. src \ dest) and (\s. cte_wp_at' (is_derived' (ctes_of s) src cap \ cteCap) src s)\ cteInsert cap src dest \\_ s. mdb_chunked (ctes_of s)\" apply (unfold cteInsert_def updateCap_def) apply (fold revokable'_fold) apply (simp add: valid_mdb'_def split del: split_if) apply (wp updateMDB_ctes_of_no_0 getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of simp del: fun_upd_apply) apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift setUntypedCapAsFull_ctes_of setUntypedCapAsFull_ctes_of_no_0 mdb_inv_preserve_modify_map setUntypedCapAsFull_mdb_chunked mdb_inv_preserve_fun_upd,simp) apply (wp getCTE_wp) apply (clarsimp simp:cte_wp_at_ctes_of simp del:fun_upd_apply) apply (subgoal_tac "src \ 0") prefer 2 apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (subgoal_tac "dest \ 0") prefer 2 apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (rule conjI) apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (case_tac cte) apply (rename_tac s_cap s_node) apply (case_tac cteb) apply (rename_tac d_cap d_node) apply (simp add: nullPointer_def) apply (subgoal_tac "mdb_insert (ctes_of s) src s_cap s_node dest NullCap d_node") apply (drule mdb_insert.chunked_n, erule is_derived_badge_derived') apply (clarsimp simp: modify_map_apply mdb_chunked_prev_update) apply unfold_locales apply (assumption|rule refl)+ apply (simp add: valid_mdb_ctes_def) apply (simp add: valid_mdb_ctes_def) apply assumption done lemma cteInsert_untyped_mdb: "\valid_mdb' and pspace_distinct' and pspace_aligned' and (\s. src \ dest) and (\s. cte_wp_at' (is_derived' (ctes_of s) src cap \ cteCap) src s)\ cteInsert cap src dest \\_ s. untyped_mdb' (ctes_of s)\" apply (unfold cteInsert_def updateCap_def) apply (simp add: valid_mdb'_def split del: split_if) apply (fold revokable'_fold) apply (wp updateMDB_ctes_of_no_0 getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of simp del: fun_upd_apply) apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift setUntypedCapAsFull_ctes_of setUntypedCapAsFull_ctes_of_no_0 mdb_inv_preserve_modify_map setUntypedCapAsFull_untyped_mdb' mdb_inv_preserve_fun_upd,simp) apply (wp getCTE_wp) apply (clarsimp simp:cte_wp_at_ctes_of simp del:fun_upd_apply) apply (subgoal_tac "src \ 0") prefer 2 apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (subgoal_tac "dest \ 0") prefer 2 apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (rule conjI) apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (case_tac cte) apply (rename_tac s_cap s_node) apply (case_tac cteb) apply (rename_tac d_cap d_node) apply (simp add: nullPointer_def) apply (subgoal_tac "mdb_insert_der (ctes_of s) src s_cap s_node dest NullCap d_node cap") prefer 2 apply unfold_locales[1] apply (assumption|rule refl)+ apply (simp add: valid_mdb_ctes_def) apply (simp add: valid_mdb_ctes_def) apply assumption apply assumption apply (case_tac "isMDBParentOf (CTE s_cap s_node) (CTE cap (mdbFirstBadged_update (\a. revokable' s_cap cap) (mdbRevocable_update (\a. revokable' s_cap cap) (mdbPrev_update (\a. src) s_node))))") apply (subgoal_tac "mdb_insert_child (ctes_of s) src s_cap s_node dest NullCap d_node cap") prefer 2 apply (simp add: mdb_insert_child_def mdb_insert_child_axioms_def) apply (drule mdb_insert_child.untyped_mdb_n) apply (clarsimp simp: modify_map_apply untyped_mdb_prev_update descendants_of_prev_update) apply (subgoal_tac "mdb_insert_sib (ctes_of s) src s_cap s_node dest NullCap d_node cap") prefer 2 apply (simp add: mdb_insert_sib_def mdb_insert_sib_axioms_def) apply (drule mdb_insert_sib.untyped_mdb_n) apply (clarsimp simp: modify_map_apply untyped_mdb_prev_update descendants_of_prev_update) done lemma valid_mdb_ctes_maskedAsFull: "\valid_mdb_ctes m;m src = Some (CTE s_cap s_node)\ \ valid_mdb_ctes (m(src \ CTE (maskedAsFull s_cap cap) s_node))" apply (clarsimp simp:fun_upd_apply maskedAsFull_def) apply (intro conjI impI) apply (frule mdb_inv_preserve_updateCap [where m = m and slot = src and index = "max_free_index (capBlockSize cap)"]) apply simp apply (drule mdb_inv_preserve_sym) apply (clarsimp simp:valid_mdb_ctes_def modify_map_def) apply (frule mdb_inv_preserve.preserve_stuff,simp) apply (frule mdb_inv_preserve.by_products,simp) apply (rule mdb_inv_preserve.untyped_inc') apply (erule mdb_inv_preserve_sym) apply (clarsimp split:split_if_asm simp: isCap_simps max_free_index_def) apply simp apply (subgoal_tac "m = m(src \ CTE s_cap s_node)") apply simp apply (rule ext) apply clarsimp done lemma capAligned_maskedAsFull: "capAligned s_cap \ capAligned (maskedAsFull s_cap cap)" apply (case_tac s_cap) apply (clarsimp simp:isCap_simps capAligned_def maskedAsFull_def max_free_index_def)+ done lemma maskedAsFull_derived': "\m src = Some (CTE s_cap s_node); is_derived' m ptr b c\ \ is_derived' (m(src \ CTE (maskedAsFull s_cap cap) s_node)) ptr b c" apply (subgoal_tac "m(src \ CTE (maskedAsFull s_cap cap) s_node) = (modify_map m src (cteCap_update (\_. maskedAsFull s_cap cap)))") apply simp apply (clarsimp simp:maskedAsFull_def is_derived'_def) apply (intro conjI impI) apply (simp add:modify_map_def del:cteCap_update.simps) apply (subst same_master_descendants) apply simp apply (clarsimp simp:isCap_simps capASID_def )+ apply (clarsimp simp:modify_map_def) done lemma maskedAsFull_usable_empty: "\capMasterCap cap = capMasterCap s_cap; isUntypedCap (maskedAsFull s_cap cap)\ \ usableUntypedRange (maskedAsFull s_cap cap) = {}" apply (simp add:isCap_simps maskedAsFull_def max_free_index_def split:split_if_asm) apply fastforce+ done lemma capAligned_master: "\capAligned cap; capMasterCap cap = capMasterCap ncap\ \ capAligned ncap" apply (case_tac cap) apply (clarsimp simp:capAligned_def)+ apply (rename_tac arch_capability) apply (case_tac arch_capability) apply (clarsimp simp:capAligned_def)+ done lemma cteInsert_untyped_inc': "\valid_mdb' and pspace_distinct' and pspace_aligned' and valid_objs' and (\s. src \ dest) and (\s. cte_wp_at' (is_derived' (ctes_of s) src cap \ cteCap) src s)\ cteInsert cap src dest \\_ s. untyped_inc' (ctes_of s)\" apply (unfold cteInsert_def updateCap_def) apply (simp add: valid_mdb'_def split del: split_if) apply (fold revokable'_fold) apply (wp updateMDB_ctes_of_no_0 getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of simp del: fun_upd_apply) apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift setUntypedCapAsFull_ctes_of setUntypedCapAsFull_ctes_of_no_0 mdb_inv_preserve_modify_map setUntypedCapAsFull_untyped_mdb' mdb_inv_preserve_fun_upd) apply (wp getCTE_wp setUntypedCapAsFull_ctes) apply (clarsimp simp:cte_wp_at_ctes_of simp del:fun_upd_apply) apply (subgoal_tac "src \ 0") prefer 2 apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (subgoal_tac "dest \ 0") prefer 2 apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (rule conjI) apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (case_tac cte) apply (rename_tac s_cap s_node) apply (case_tac cteb) apply (rename_tac d_cap d_node) apply (simp add: nullPointer_def) apply (subgoal_tac "mdb_insert_der (modify_map (ctes_of s) src (cteCap_update (\_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest NullCap d_node cap") prefer 2 apply unfold_locales[1] apply (clarsimp simp:modify_map_def valid_mdb_ctes_maskedAsFull)+ apply (erule(2) valid_mdb_ctesE[OF valid_mdb_ctes_maskedAsFull]) apply (clarsimp simp:modify_map_def) apply (erule(2) valid_mdb_ctesE[OF valid_mdb_ctes_maskedAsFull]) apply simp apply (clarsimp simp:modify_map_def maskedAsFull_derived') apply (case_tac "isMDBParentOf (CTE (maskedAsFull s_cap cap) s_node) (CTE cap (mdbFirstBadged_update (\a. revokable' (maskedAsFull s_cap cap) cap) (mdbRevocable_update (\a. revokable' (maskedAsFull s_cap cap) cap) (mdbPrev_update (\a. src) s_node))))") apply (subgoal_tac "mdb_insert_child (modify_map (ctes_of s) src (cteCap_update (\_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest NullCap d_node cap") prefer 2 apply (simp add: mdb_insert_child_def mdb_insert_child_axioms_def) apply (drule mdb_insert_child.untyped_inc_n) apply (rule capAligned_maskedAsFull[OF valid_capAligned]) apply (erule(1) ctes_of_valid_cap') apply (intro impI maskedAsFull_usable_empty) apply (clarsimp simp:is_derived'_def badge_derived'_def) apply simp apply (clarsimp simp: modify_map_apply untyped_inc_prev_update maskedAsFull_revokable descendants_of_prev_update) apply (subgoal_tac "mdb_insert_sib (modify_map (ctes_of s) src (cteCap_update (\_. maskedAsFull s_cap cap))) src (maskedAsFull s_cap cap) s_node dest NullCap d_node cap") prefer 2 apply (simp add: mdb_insert_sib_def mdb_insert_sib_axioms_def) apply (drule mdb_insert_sib.untyped_inc_n) apply (rule capAligned_master[OF valid_capAligned]) apply (erule(1) ctes_of_valid_cap') apply (clarsimp simp:is_derived'_def badge_derived'_def) apply (clarsimp simp: modify_map_apply untyped_inc_prev_update maskedAsFull_revokable descendants_of_prev_update) done lemma irq_control_prev_update: "irq_control (modify_map m x (cteMDBNode_update (mdbPrev_update f))) = irq_control m" apply (simp add: irq_control_def) apply (rule iffI) apply clarsimp apply (simp only: modify_map_if) apply (erule_tac x=p in allE) apply (simp (no_asm_use) split: split_if_asm) apply (case_tac "x=p") apply fastforce apply clarsimp apply (erule_tac x=p' in allE) apply simp apply (case_tac "x=p'") apply simp apply fastforce apply clarsimp apply (erule_tac x=p in allE) apply (simp add: modify_map_if split: split_if_asm) apply clarsimp apply (case_tac "x=p'") apply clarsimp apply clarsimp apply clarsimp apply (case_tac "x=p'") apply clarsimp apply clarsimp done lemma cteInsert_irq_control: "\valid_mdb' and pspace_distinct' and pspace_aligned' and (\s. src \ dest) and (\s. cte_wp_at' (is_derived' (ctes_of s) src cap \ cteCap) src s)\ cteInsert cap src dest \\_ s. irq_control (ctes_of s)\" apply (unfold cteInsert_def updateCap_def) apply (simp add: valid_mdb'_def split del: split_if) apply (fold revokable'_fold) apply (wp updateMDB_ctes_of_no_0 getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of simp del: fun_upd_apply) apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift setUntypedCapAsFull_ctes_of setUntypedCapAsFull_ctes_of_no_0 setUntypedCapAsFull_irq_control mdb_inv_preserve_fun_upd mdb_inv_preserve_modify_map,simp) apply (wp getCTE_wp) apply (clarsimp simp:cte_wp_at_ctes_of simp del:fun_upd_apply) apply (subgoal_tac "src \ 0") prefer 2 apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (subgoal_tac "dest \ 0") prefer 2 apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (rule conjI) apply (fastforce simp: valid_mdb_ctes_def no_0_def) apply (case_tac cte) apply (rename_tac s_cap s_node) apply (case_tac cteb) apply (rename_tac d_cap d_node) apply (simp add: nullPointer_def) apply (subgoal_tac "mdb_insert_der (ctes_of s) src s_cap s_node dest NullCap d_node cap") prefer 2 apply unfold_locales[1] apply (assumption|rule refl)+ apply (simp add: valid_mdb_ctes_def) apply (simp add: valid_mdb_ctes_def) apply assumption+ apply (drule mdb_insert_der.irq_control_n) apply (clarsimp simp: modify_map_apply irq_control_prev_update) done lemma capMaster_isUntyped: "capMasterCap c = capMasterCap c' \ isUntypedCap c = isUntypedCap c'" by (simp add: capMasterCap_def isCap_simps split: capability.splits) lemma capMaster_capRange: "capMasterCap c = capMasterCap c' \ capRange c = capRange c'" by (simp add: capMasterCap_def capRange_def split: capability.splits arch_capability.splits) lemma capMaster_untypedRange: "capMasterCap c = capMasterCap c' \ untypedRange c = untypedRange c'" by (simp add: capMasterCap_def capRange_def split: capability.splits arch_capability.splits) lemma capMaster_capClass: "capMasterCap c = capMasterCap c' \ capClass c = capClass c'" by (simp add: capMasterCap_def split: capability.splits arch_capability.splits) lemma valid_dlist_no_0_prev: "\ m p = Some (CTE c n); m (mdbNext n) = Some (CTE c' (MDB x 0 b1 b2)); valid_dlist m; no_0 m \ \ False" apply (erule (1) valid_dlistE) apply clarsimp apply clarsimp done lemma distinct_zombies_nonCTE_modify_map: "\m x f. \ \cte. cteCap (f cte) = cteCap cte \ \ distinct_zombies (modify_map m x f) = distinct_zombies m" apply (simp add: distinct_zombies_def modify_map_def o_def) apply (rule_tac f=distinct_zombie_caps in arg_cong) apply (rule ext) apply simp apply (simp add: map_option.compositionality o_def) done lemma setUntypedCapAsFull_ctes_of_no_0': "\\s. no_0 (ctes_of s) \ cte_wp_at' (op = srcCTE) src s\ setUntypedCapAsFull (cteCap srcCTE) cap src \\r s. no_0 (ctes_of s)\" apply (clarsimp simp:no_0_def split:if_splits) apply (wp hoare_vcg_imp_lift setUntypedCapAsFull_ctes_of[where dest = 0]) apply (auto simp:cte_wp_at_ctes_of) done (* FIXME: move *) lemma mdb_inv_preserve_update_cap_same: "mdb_inv_preserve m m' \ mdb_inv_preserve (modify_map m dest (cteCap_update (\_. cap))) (modify_map m' dest (cteCap_update (\_. cap)))" apply (simp (no_asm) add:mdb_inv_preserve_def) apply (intro conjI allI) apply (drule mdb_inv_preserve.dom) apply (simp add:modify_map_dom) apply (clarsimp simp:modify_map_def split del:if_splits split:split_if_asm) apply (drule(2) mdb_inv_preserve.misc,simp)+ apply (clarsimp simp:mdb_inv_preserve.sameRegion modify_map_def split:if_splits)+ apply (case_tac "p = dest") apply (clarsimp simp:mdb_next_def option_map_def split:option.splits ) apply (intro conjI allI impI) apply (rule ccontr,clarify) apply (fastforce dest!:iffD2[OF mdb_inv_preserve.dom,OF _ domI]) apply (rule ccontr,simp) apply (fastforce dest!:iffD1[OF mdb_inv_preserve.dom,OF _ domI]) apply (drule mdb_inv_preserve.mdb_next[where p = dest]) apply (clarsimp simp:mdb_next_def option_map_def split:option.splits)+ apply (intro conjI allI impI) apply (rule ccontr,clarify) apply (fastforce dest!:iffD2[OF mdb_inv_preserve.dom,OF _ domI]) apply (rule ccontr,simp) apply (fastforce dest!:iffD1[OF mdb_inv_preserve.dom,OF _ domI]) apply (drule_tac p = p in mdb_inv_preserve.mdb_next) apply (clarsimp simp:mdb_next_def option_map_def split:option.splits) done lemma updateCapFreeIndex_dlist: assumes preserve:"\m m'. mdb_inv_preserve m m' \ mdb_inv_preserve (Q m) (Q m')" shows "\\s. P (valid_dlist (Q (ctes_of s))) \ cte_wp_at' (\c. c = srcCTE \ isUntypedCap (cteCap c)) src s\ updateCap src (capFreeIndex_update (\_. index) (cteCap srcCTE)) \\r s. P (valid_dlist (Q (ctes_of s)))\" apply (wp updateCap_ctes_of_wp) apply (subgoal_tac "mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\_. capFreeIndex_update (\_. index) (cteCap srcCTE)))))") apply (drule mdb_inv_preserve.preserve_stuff) apply simp apply (rule preserve) apply (rule mdb_inv_preserve_updateCap) apply (clarsimp simp:cte_wp_at_ctes_of)+ done lemma setUntypedCapAsFull_valid_dlist: assumes preserve: "\m m'. mdb_inv_preserve m m' \ mdb_inv_preserve (Q m) (Q m')" shows "\\s. P (valid_dlist (Q (ctes_of s))) \ cte_wp_at' (\c. c = srcCTE) src s\ setUntypedCapAsFull (cteCap srcCTE) cap src \\r s. P (valid_dlist (Q (ctes_of s)))\" apply (clarsimp simp:setUntypedCapAsFull_def split:if_splits,intro conjI impI) apply (wp updateCapFreeIndex_dlist) apply (clarsimp simp:preserve cte_wp_at_ctes_of)+ apply wp apply clarsimp done lemma valid_dlist_prevD: "\m p = Some cte;valid_dlist m;mdbPrev (cteMDBNode cte) \ 0\ \ (\cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \ mdbNext (cteMDBNode cte') = p)" by (clarsimp simp:valid_dlist_def Let_def) lemma valid_dlist_nextD: "\m p = Some cte;valid_dlist m;mdbNext (cteMDBNode cte) \ 0\ \ (\cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \ mdbPrev (cteMDBNode cte') = p)" by (clarsimp simp:valid_dlist_def Let_def) lemma no_loops_no_l2_loop: "\valid_dlist m; no_loops m; m p = Some cte;mdbPrev (cteMDBNode cte) = mdbNext (cteMDBNode cte)\ \ mdbNext (cteMDBNode cte) = 0" apply (rule ccontr) apply (subgoal_tac "m \ p \ (mdbNext (cteMDBNode cte))") prefer 2 apply (clarsimp simp:mdb_next_rel_def mdb_next_def) apply (subgoal_tac "m \ (mdbNext (cteMDBNode cte)) \ p") prefer 2 apply (clarsimp simp:mdb_next_rel_def mdb_next_def) apply (frule(2) valid_dlist_nextD) apply clarsimp apply (frule(1) valid_dlist_prevD) apply simp+ apply (drule(1) transitive_closure_trans) apply (simp add:no_loops_def) done lemma cteInsert_no_0: "\valid_mdb' and pspace_aligned' and pspace_distinct' and (\s. src \ dest) and K (capAligned cap) and valid_objs' and (\s. cte_wp_at' (is_derived' (ctes_of s) src cap \ cteCap) src s)\ cteInsert cap src dest \\_ s. no_0 (ctes_of s) \" apply (rule hoare_name_pre_state) apply clarsimp apply (unfold cteInsert_def updateCap_def) apply (simp add: valid_mdb'_def split del: split_if) apply (fold revokable'_fold) apply (wp updateMDB_ctes_of_no_0 getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of simp del: fun_upd_apply) apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift setUntypedCapAsFull_ctes_of setUntypedCapAsFull_ctes_of_no_0 mdb_inv_preserve_modify_map getCTE_wp setUntypedCapAsFull_valid_dlist mdb_inv_preserve_fun_upd | simp)+ apply (intro conjI impI) apply (clarsimp simp:cte_wp_at_ctes_of) apply (clarsimp simp:valid_mdb_ctes_def no_0_def) done lemma cteInsert_valid_dlist: "\valid_mdb' and pspace_aligned' and pspace_distinct' and (\s. src \ dest) and K (capAligned cap) and valid_objs' and (\s. cte_wp_at' (is_derived' (ctes_of s) src cap \ cteCap) src s)\ cteInsert cap src dest \\_ s. valid_dlist (ctes_of s) \" apply (rule hoare_name_pre_state) apply clarsimp apply (unfold cteInsert_def updateCap_def) apply (simp add: valid_mdb'_def split del: split_if) apply (fold revokable'_fold) apply (wp updateMDB_ctes_of_no_0 getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of simp del: fun_upd_apply) apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift setUntypedCapAsFull_ctes_of setUntypedCapAsFull_ctes_of_no_0 mdb_inv_preserve_modify_map getCTE_wp setUntypedCapAsFull_valid_dlist mdb_inv_preserve_fun_upd | simp)+ apply (intro conjI impI) apply (clarsimp simp:cte_wp_at_ctes_of) apply (intro conjI) apply (clarsimp simp:valid_mdb_ctes_def no_0_def)+ apply (frule mdb_chain_0_no_loops) apply (simp add:no_0_def) apply (rule valid_dlistI) apply (case_tac "p = dest") apply (clarsimp simp:modify_map_def nullPointer_def split:split_if_asm)+ apply (frule(2) valid_dlist_prevD) apply simp apply (subgoal_tac "mdbPrev (cteMDBNode ctea) \ mdbNext (cteMDBNode ctea)") prefer 2 apply (clarsimp) apply (drule(3) no_loops_no_l2_loop[rotated -1],simp) apply (subgoal_tac "mdbPrev (cteMDBNode ctea) \ dest") apply clarsimp+ apply (frule_tac p = p and m = "ctes_of sa" in valid_dlist_prevD) apply simp+ apply fastforce apply (case_tac "p = dest") apply (clarsimp simp:modify_map_def nullPointer_def split:split_if_asm)+ apply (frule(2) valid_dlist_nextD,clarsimp) apply (clarsimp simp:modify_map_def nullPointer_def split:split_if_asm) apply (frule(2) valid_dlist_nextD) apply simp apply (subgoal_tac "mdbPrev (cteMDBNode ctea) \ mdbNext (cteMDBNode ctea)") prefer 2 apply (clarsimp) apply (drule(3) no_loops_no_l2_loop[rotated -1],simp) apply clarsimp apply (intro conjI impI) apply clarsimp+ apply (drule_tac cte = cte' in no_loops_no_l2_loop,simp) apply simp+ apply (frule(2) valid_dlist_nextD) apply clarsimp apply (frule_tac p = p and m = "ctes_of sa" in valid_dlist_nextD) apply clarsimp+ apply (rule conjI) apply fastforce apply (intro conjI impI,clarsimp+) apply (frule_tac valid_dlist_nextD) apply clarsimp+ apply (frule_tac valid_dlist_nextD) apply clarsimp+ done lemma cteInsert_mdb' [wp]: "\valid_mdb' and pspace_aligned' and pspace_distinct' and (\s. src \ dest) and K (capAligned cap) and valid_objs' and (\s. cte_wp_at' (is_derived' (ctes_of s) src cap \ cteCap) src s) \ cteInsert cap src dest \\_. valid_mdb'\" apply (simp add:valid_mdb'_def valid_mdb_ctes_def revokable'_fold[symmetric]) apply (rule_tac Q = "\r s. valid_dlist (ctes_of s) \ irq_control (ctes_of s) \ no_0 (ctes_of s) \ mdb_chain_0 (ctes_of s) \ mdb_chunked (ctes_of s) \ untyped_mdb' (ctes_of s) \ untyped_inc' (ctes_of s) \ Q s" for Q in hoare_strengthen_post) prefer 2 apply clarsimp apply assumption apply (rule hoare_name_pre_state) apply (wp cteInsert_no_0 cteInsert_valid_dlist cteInsert_mdb_chain_0 cteInsert_untyped_inc' cteInsert_mdb_chunked cteInsert_untyped_mdb cteInsert_irq_control) apply (unfold cteInsert_def) apply (unfold cteInsert_def updateCap_def) apply (simp add: valid_mdb'_def split del: split_if) apply (fold revokable'_fold) apply (wp updateMDB_ctes_of_no_0 getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of simp del: fun_upd_apply) apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift setUntypedCapAsFull_ctes_of setUntypedCapAsFull_ctes_of_no_0 setUntypedCapAsFull_valid_dlist setUntypedCapAsFull_distinct_zombies setUntypedCapAsFull_valid_badges setUntypedCapAsFull_caps_contained setUntypedCapAsFull_valid_nullcaps setUntypedCapAsFull_ut_revocable setUntypedCapAsFull_class_links setUntypedCapAsFull_reply_masters_rvk_fb mdb_inv_preserve_fun_upd mdb_inv_preserve_modify_map getCTE_wp| simp del:fun_upd_apply)+ apply (clarsimp simp:cte_wp_at_ctes_of simp del:fun_upd_apply) defer apply (clarsimp simp:valid_mdb_ctes_def valid_mdb'_def simp del:fun_upd_apply)+ apply (case_tac cte) apply (rename_tac cap1 node1) apply (case_tac x) apply (rename_tac cap2 node2) apply (case_tac node1) apply (case_tac node2) apply (clarsimp simp:valid_mdb_ctes_def no_0_def nullPointer_def) apply (intro conjI impI) apply clarsimp apply (rename_tac s src_cap word1 word2 bool1a bool2a bool1 bool2) proof - fix s :: kernel_state fix bool1 bool2 src_cap word1 word2 bool1a bool2a let ?c1 = "(CTE src_cap (MDB word1 word2 bool1a bool2a))" let ?c2 = "(CTE capability.NullCap (MDB 0 0 bool1 bool2))" let ?C = "(modify_map (modify_map (modify_map (ctes_of s(dest \ CTE cap (MDB 0 0 bool1 bool2))) dest (cteMDBNode_update (\a. MDB word1 src (revokable' src_cap cap) (revokable' src_cap cap)))) src (cteMDBNode_update (mdbNext_update (\_. dest)))) word1 (cteMDBNode_update (mdbPrev_update (\_. dest))))" let ?m = "ctes_of s" let ?prv = "\cte. mdbPrev (cteMDBNode cte)" let ?nxt = "\cte. mdbNext (cteMDBNode cte)" assume "pspace_distinct' s" and "pspace_aligned' s" and srcdest: "src \ dest" and dest0: "dest \ 0" and cofs: "ctes_of s src = Some ?c1" and cofd: "ctes_of s dest = Some ?c2" and is_der: "is_derived' (ctes_of s) src cap src_cap" and aligned: "capAligned cap" and vd: "valid_dlist ?m" and no0: "?m 0 = None" and chain: "mdb_chain_0 ?m" and badges: "valid_badges ?m" and chunk: "mdb_chunked ?m" and contained: "caps_contained' ?m" and untyped_mdb: "untyped_mdb' ?m" and untyped_inc: "untyped_inc' ?m" and class_links: "class_links ?m" and distinct_zombies: "distinct_zombies ?m" and irq: "irq_control ?m" and reply_masters_rvk_fb: "reply_masters_rvk_fb ?m" and vn: "valid_nullcaps ?m" and ut_rev:"ut_revocable' ?m" have no_loop: "no_loops ?m" apply (rule mdb_chain_0_no_loops[OF chain]) apply (simp add:no_0_def no0) done have badge: "badge_derived' cap src_cap" using is_der by (clarsimp simp:is_derived'_def) have vmdb: "valid_mdb_ctes ?m" by (auto simp: vmdb_def valid_mdb_ctes_def no_0_def, fact+) have src0: "src \ 0" using cofs no0 by clarsimp have destnull: "cte_mdb_prop ?m dest (\m. mdbPrev m = 0 \ mdbNext m = 0)" using cofd unfolding cte_mdb_prop_def by auto have srcwd: "?m \ src \ word1" using cofs by (simp add: next_unfold') have w1ned[simp]: "word1 \ dest" proof (cases "word1 = 0") case True thus ?thesis using dest0 by auto next case False thus ?thesis using cofs cofd src0 dest0 False vd by - (erule (1) valid_dlistEn, (clarsimp simp: nullPointer_def)+) qed have w2ned[simp]: "word2 \ dest" proof (cases "word2 = 0") case True thus ?thesis using dest0 by auto next case False thus ?thesis using cofs cofd src0 dest0 False vd by - (erule (1) valid_dlistEp, (clarsimp simp: nullPointer_def)+) qed have w1nes[simp]: "word1 \ src" using vmdb cofs by - (drule (1) no_self_loop_next, simp) have w2nes[simp]: "word2 \ src" using vmdb cofs by - (drule (1) no_self_loop_prev, simp) from is_der have notZomb1: "\ isZombie cap" by (clarsimp simp: isCap_simps is_derived'_def badge_derived'_def) from is_der have notZomb2: "\ isZombie src_cap" by (clarsimp simp: isCap_simps is_derived'_def) from badge have masters: "capMasterCap cap = capMasterCap src_cap" by (clarsimp simp: badge_derived'_def) note blah[simp] = w2nes[symmetric] w1nes[symmetric] w1ned[symmetric] w2ned[symmetric] srcdest srcdest[symmetric] have mdb_next_disj: "\p p'. (?C \ p \ p' \ ?m \ p \ p' \ p \ src \ p'\ dest \ (p' = word1 \ p' = 0) \ p = src \ p' = dest \ p = dest \ p' = word1)" apply (case_tac "p = src") apply (clarsimp simp:mdb_next_unfold modify_map_cases) apply (case_tac "p = dest") apply (clarsimp simp:mdb_next_unfold modify_map_cases)+ using cofs cofd vd no0 apply - apply (case_tac "p = word1") apply clarsimp apply (intro conjI) apply clarsimp apply (frule_tac p = "word1" and m = "?m" in valid_dlist_nextD) apply clarsimp+ apply (frule_tac p = "mdbNext node" and m = "?m" in valid_dlist_nextD) apply clarsimp+ apply (frule_tac p = "mdbNext node" in no_loops_no_l2_loop[OF _ no_loop]) apply simp+ apply (intro conjI) apply clarsimp apply (frule_tac p = p and m = "?m" in valid_dlist_nextD) apply (clarsimp+)[3] apply (intro impI) apply (rule ccontr) apply clarsimp apply (frule_tac p = src and m = "?m" in valid_dlist_nextD) apply clarsimp+ apply (frule_tac p = p and m = "?m" in valid_dlist_nextD) apply clarsimp+ done have ctes_ofD: "\p cte. \?C p = Some cte; p\ dest; p\ src\ \ \cteb. (?m p = Some cteb \ cteCap cte = cteCap cteb)" by (clarsimp simp:modify_map_def split:if_splits) show "valid_badges ?C" using srcdest badge cofs badges cofd unfolding valid_badges_def apply (intro impI allI) apply (drule mdb_next_disj) apply (elim disjE) defer apply (clarsimp simp:modify_map_cases dest0 src0) apply (clarsimp simp:revokable'_def badge_derived'_def) subgoal by (case_tac src_cap,auto simp:isCap_simps sameRegionAs_def) apply (clarsimp simp:modify_map_cases valid_badges_def) apply (frule_tac x=src in spec, erule_tac x=word1 in allE, erule allE, erule impE) apply fastforce apply simp apply (clarsimp simp:mdb_next_unfold badge_derived'_def split: split_if_asm) apply (thin_tac "All P" for P) subgoal by (cases src_cap, auto simp:mdb_next_unfold isCap_simps sameRegionAs_def Let_def split: if_splits) apply (case_tac "word1 = p'") apply (clarsimp simp:modify_map_cases valid_badges_def mdb_next_unfold src0 dest0 no0)+ apply (case_tac "p = dest") apply (clarsimp simp:dest0 src0 no0)+ apply (case_tac z) apply (rename_tac capability mdbnode) apply clarsimp apply (drule_tac x = p in spec,drule_tac x = "mdbNext mdbnode" in spec) by (auto simp:isCap_simps sameRegionAs_def) from badge have isUntyped_eq: "isUntypedCap cap = isUntypedCap src_cap" apply (clarsimp simp:badge_derived'_def) apply (case_tac cap,auto simp:isCap_simps) done from badge have [simp]: "capRange cap = capRange src_cap" apply (clarsimp simp:badge_derived'_def) apply (case_tac cap) apply (clarsimp simp:isCap_simps capRange_def)+ (* 5 subgoals *) apply (rename_tac arch_capability) apply (case_tac arch_capability) (* 9 subgoals *) apply (clarsimp simp:isCap_simps capRange_def)+ done have [simp]: "untypedRange cap = untypedRange src_cap" using badge apply (clarsimp simp:badge_derived'_def dest!:capMaster_untypedRange) done from contained badge srcdest cofs cofd is_der no0 show "caps_contained' ?C" apply (clarsimp simp add: caps_contained'_def) apply (case_tac "p = dest") apply (case_tac "p' = dest") apply (clarsimp simp:modify_map_def split:if_splits) apply (case_tac src_cap,auto)[1] apply (case_tac "p' = src") apply (clarsimp simp:modify_map_def split:if_splits) apply (clarsimp simp:badge_derived'_def) apply (case_tac src_cap,auto)[1] apply (drule(2) ctes_ofD) apply (clarsimp simp:modify_map_def split:if_splits) apply (frule capRange_untyped) apply (erule_tac x=src in allE, erule_tac x=p' in allE, simp) apply (case_tac cteb) apply (clarsimp) apply blast apply (case_tac "p' = dest") apply (case_tac "p = src") apply (clarsimp simp:modify_map_def split:if_splits) apply (drule capRange_untyped) subgoal by (case_tac cap,auto simp:isCap_simps badge_derived'_def) apply (clarsimp simp:modify_map_def split:if_splits) apply (drule_tac x = word1 in spec) apply (drule_tac x = src in spec) apply (case_tac z) apply (clarsimp simp:isUntyped_eq) apply blast apply (drule_tac x = p in spec) apply (drule_tac x = src in spec) apply (frule capRange_untyped) apply (clarsimp simp:isUntyped_eq) apply blast apply (drule_tac x = p in spec) apply (drule_tac x = p' in spec) apply (clarsimp simp:modify_map_def split:if_splits) apply ((case_tac z,fastforce)+)[5] by fastforce+ show "valid_nullcaps ?C" using is_der vn cofs vd no0 apply (simp add: valid_nullcaps_def srcdest [symmetric]) apply (clarsimp simp:modify_map_def is_derived'_def) apply (rule conjI) apply (clarsimp simp: is_derived'_def badge_derived'_def)+ apply (drule_tac x = word1 in spec) apply (case_tac z) apply (clarsimp simp:nullMDBNode_def) apply (drule(1) valid_dlist_nextD) apply simp apply clarsimp apply (simp add:nullPointer_def src0) done from vmdb srcdest cofs ut_rev show "ut_revocable' ?C" apply (clarsimp simp: valid_mdb_ctes_def ut_revocable'_def modify_map_def) apply (rule conjI) apply clarsimp apply (clarsimp simp: revokable'_def isCap_simps)+ apply auto apply (drule_tac x= src in spec) apply clarsimp apply (case_tac z) apply clarsimp done from class_links srcdest badge cofs cofd no0 vd show "class_links ?C" unfolding class_links_def apply (intro allI impI) apply (drule mdb_next_disj) apply (elim disjE) apply (clarsimp simp:modify_map_def mdb_next_unfold split:split_if_asm) apply (clarsimp simp: badge_derived'_def modify_map_def split: split_if_asm) apply (erule capMaster_capClass) apply (clarsimp simp:modify_map_def split:if_splits) apply (drule_tac x = src in spec) apply (drule_tac x = word1 in spec) apply (clarsimp simp:mdb_next_unfold) apply (case_tac z) apply (clarsimp simp:badge_derived'_def) apply (drule capMaster_capClass) apply simp done from distinct_zombies badge show "distinct_zombies ?C" apply (simp add:distinct_zombies_nonCTE_modify_map) apply (erule_tac distinct_zombies_copyMasterE[where x=src]) apply (rule cofs) apply (simp add: masters) apply (simp add: notZomb1 notZomb2) done from reply_masters_rvk_fb is_der show "reply_masters_rvk_fb ?C" apply (clarsimp simp:reply_masters_rvk_fb_def) apply (erule ranE) apply (clarsimp simp:modify_map_def split:split_if_asm) apply fastforce+ apply (clarsimp simp:is_derived'_def isCap_simps) apply fastforce done qed crunch state_refs_of'[wp]: cteInsert "\s. P (state_refs_of' s)" (wp: crunch_wps) crunch aligned'[wp]: cteInsert pspace_aligned' (wp: crunch_wps) crunch distinct'[wp]: cteInsert pspace_distinct' (wp: crunch_wps) crunch no_0_obj' [wp]: cteInsert no_0_obj' (wp: crunch_wps) lemma cteInsert_valid_pspace: "\valid_pspace' and valid_cap' cap and (\s. src \ dest) and valid_objs' and (\s. cte_wp_at' (is_derived' (ctes_of s) src cap \ cteCap) src s)\ cteInsert cap src dest \\_. valid_pspace'\" unfolding valid_pspace'_def apply (rule hoare_pre) apply (wp cteInsert_valid_objs) apply (fastforce elim: valid_capAligned) done lemma setCTE_ko_wp_at_live[wp]: "\\s. P (ko_wp_at' live' p' s)\ setCTE p v \\rv s. P (ko_wp_at' live' p' s)\" apply (clarsimp simp: setCTE_def setObject_def split_def valid_def in_monad ko_wp_at'_def split del: split_if elim!: rsubst[where P=P]) apply (drule(1) updateObject_cte_is_tcb_or_cte [OF _ refl, rotated]) apply (elim exE conjE disjE) apply (clarsimp simp: ps_clear_upd' objBits_simps lookupAround2_char1) apply (simp add: tcb_cte_cases_def split: split_if_asm) apply (clarsimp simp: ps_clear_upd' objBits_simps) done lemma setCTE_iflive': "\\s. cte_wp_at' (\cte'. \p'\zobj_refs' (cteCap cte') - zobj_refs' (cteCap cte). ko_wp_at' (Not \ live') p' s) p s \ if_live_then_nonz_cap' s\ setCTE p cte \\rv s. if_live_then_nonz_cap' s\" unfolding if_live_then_nonz_cap'_def ex_nonz_cap_to'_def apply (rule hoare_pre) apply (simp only: imp_conv_disj) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift hoare_vcg_ex_lift setCTE_weak_cte_wp_at) apply clarsimp apply (drule spec, drule(1) mp) apply clarsimp apply (rule_tac x=cref in exI) apply (clarsimp simp: cte_wp_at'_def) apply (rule ccontr) apply (drule bspec, fastforce) apply (clarsimp simp: ko_wp_at'_def) done lemma updateMDB_iflive'[wp]: "\\s. if_live_then_nonz_cap' s\ updateMDB p m \\rv s. if_live_then_nonz_cap' s\" apply (clarsimp simp: updateMDB_def) apply (rule hoare_seq_ext [OF _ getCTE_sp]) apply (wp setCTE_iflive') apply (clarsimp elim!: cte_wp_at_weakenE') done lemma updateCap_iflive': "\\s. cte_wp_at' (\cte'. \p'\zobj_refs' (cteCap cte') - zobj_refs' cap. ko_wp_at' (Not \ live') p' s) p s \ if_live_then_nonz_cap' s\ updateCap p cap \\rv s. if_live_then_nonz_cap' s\" apply (simp add: updateCap_def) apply (rule hoare_seq_ext [OF _ getCTE_sp]) apply (wp setCTE_iflive') apply (clarsimp elim!: cte_wp_at_weakenE') done lemma setCTE_ko_wp_at_not_live[wp]: "\\s. P (ko_wp_at' (Not \ live') p' s)\ setCTE p v \\rv s. P (ko_wp_at' (Not \ live') p' s)\" apply (clarsimp simp: setCTE_def setObject_def split_def valid_def in_monad ko_wp_at'_def split del: split_if elim!: rsubst[where P=P]) apply (drule(1) updateObject_cte_is_tcb_or_cte [OF _ refl, rotated]) apply (elim exE conjE disjE) apply (clarsimp simp: ps_clear_upd' objBits_simps lookupAround2_char1) apply (simp add: tcb_cte_cases_def split: split_if_asm) apply (clarsimp simp: ps_clear_upd' objBits_simps) done lemma setUntypedCapAsFull_ko_wp_not_at'[wp]: "\\s. P (ko_wp_at' (Not \ live') p' s)\ setUntypedCapAsFull (cteCap srcCTE) cap src \\r s. P ( ko_wp_at' (Not \ live') p' s)\" apply (clarsimp simp:setUntypedCapAsFull_def updateCap_def) apply (wp setCTE_ko_wp_at_live setCTE_ko_wp_at_not_live) done lemma setUntypedCapAsFull_ko_wp_at'[wp]: "\\s. P (ko_wp_at' live' p' s)\ setUntypedCapAsFull (cteCap srcCTE) cap src \\r s. P ( ko_wp_at' live' p' s)\" apply (clarsimp simp:setUntypedCapAsFull_def updateCap_def) apply (wp setCTE_ko_wp_at_live setCTE_ko_wp_at_live) done (*FIXME:MOVE*) lemma zobj_refs'_capFreeIndex_update[simp]: "isUntypedCap ctecap \ zobj_refs' (capFreeIndex_update f (ctecap)) = zobj_refs' ctecap" by (case_tac ctecap,auto simp:isCap_simps) lemma setUntypedCapAsFull_if_live_then_nonz_cap': "\\s. if_live_then_nonz_cap' s \ cte_wp_at' (op = srcCTE) src s\ setUntypedCapAsFull (cteCap srcCTE) cap src \\rv s. if_live_then_nonz_cap' s\" apply (clarsimp simp:if_live_then_nonz_cap'_def) apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift) apply (clarsimp simp:setUntypedCapAsFull_def split del:if_splits) apply (wp hoare_vcg_split_if) apply (clarsimp simp:ex_nonz_cap_to'_def cte_wp_at_ctes_of) apply (wp updateCap_ctes_of_wp) apply clarsimp apply (elim allE impE) apply (assumption) apply (clarsimp simp:ex_nonz_cap_to'_def cte_wp_at_ctes_of modify_map_def split:if_splits) apply (rule_tac x = cref in exI) apply (intro conjI impI) apply clarsimp+ done lemma maskedAsFull_simps[simp]: "maskedAsFull capability.NullCap cap = capability.NullCap" by (auto simp:maskedAsFull_def) lemma cteInsert_iflive'[wp]: "\\s. if_live_then_nonz_cap' s \ cte_wp_at' (\c. cteCap c = NullCap) dest s\ cteInsert cap src dest \\rv. if_live_then_nonz_cap'\" apply (rule hoare_pre) apply (simp add: cteInsert_def split del: split_if) apply (wp updateCap_iflive' hoare_drop_imps) apply (clarsimp simp:cte_wp_at_ctes_of) apply (wp hoare_vcg_conj_lift hoare_vcg_ex_lift hoare_vcg_ball_lift getCTE_wp setUntypedCapAsFull_ctes_of setUntypedCapAsFull_if_live_then_nonz_cap') apply (clarsimp simp:cte_wp_at_ctes_of) apply (intro conjI) apply (rule_tac x = "case (ctes_of s dest) of Some a \a" in exI) apply (intro conjI impI) apply (clarsimp) apply (case_tac cte,simp) apply clarsimp+ done lemma ifunsafe'_def2: "if_unsafe_then_cap' = (\s. \cref cte. ctes_of s cref = Some cte \ cteCap cte \ NullCap \ (\cref' cte'. ctes_of s cref' = Some cte' \ cref \ cte_refs' (cteCap cte') (irq_node' s)))" by (clarsimp intro!: ext simp: if_unsafe_then_cap'_def cte_wp_at_ctes_of ex_cte_cap_to'_def) lemma ifunsafe'_def3: "if_unsafe_then_cap' = (\s. \cref cap. cteCaps_of s cref = Some cap \ cap \ NullCap \ (\cref' cap'. cteCaps_of s cref' = Some cap' \ cref \ cte_refs' cap' (irq_node' s)))" apply (simp add: cteCaps_of_def o_def ifunsafe'_def2) apply (fastforce intro!: ext) done lemma tree_cte_cteCap_eq: "cte_wp_at' (P \ cteCap) p s = (case_option False P (cteCaps_of s p))" apply (simp add: cte_wp_at_ctes_of cteCaps_of_def) apply (cases "ctes_of s p", simp_all) done lemma updateMDB_cteCaps_of: "\\s. P (cteCaps_of s)\ updateMDB ptr f \\rv s. P (cteCaps_of s)\" apply (simp add: cteCaps_of_def) apply (wp updateMDB_ctes_of_wp) apply (safe elim!: rsubst [where P=P] intro!: ext) apply (case_tac "ctes_of s x") apply (clarsimp simp: modify_map_def)+ done lemma setCTE_ksInterruptState[wp]: "\\s. P (ksInterruptState s)\ setCTE param_a param_b \\_ s. P (ksInterruptState s)\" by (wp setObject_ksInterrupt updateObject_cte_inv | simp add: setCTE_def)+ crunch ksInterruptState[wp]: cteInsert "\s. P (ksInterruptState s)" (ignore: setObject wp: crunch_wps) lemmas updateMDB_cteCaps_of_ksInt[wp] = hoare_use_eq [where f=ksInterruptState, OF updateMDB_ksInterruptState updateMDB_cteCaps_of] lemma updateCap_cteCaps_of: "\\s. P (modify_map (cteCaps_of s) ptr (K cap))\ updateCap ptr cap \\rv s. P (cteCaps_of s)\" apply (simp add: cteCaps_of_def) apply (wp updateCap_ctes_of_wp) apply (erule rsubst [where P=P]) apply (case_tac "ctes_of s ptr") apply (clarsimp intro!: ext simp: modify_map_def)+ done lemmas updateCap_cteCaps_of_int[wp] = hoare_use_eq[where f=ksInterruptState, OF updateCap_ksInterruptState updateCap_cteCaps_of] lemma getCTE_cteCap_wp: "\\s. case (cteCaps_of s ptr) of None \ True | Some cap \ Q cap s\ getCTE ptr \\rv. Q (cteCap rv)\" apply (wp getCTE_wp) apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of) done lemma capFreeIndex_update_cte_refs'[simp]: "isUntypedCap a \ cte_refs' (capFreeIndex_update f a) = cte_refs' a " apply (rule ext) apply (clarsimp simp:isCap_simps) done lemma cteInsert_ifunsafe'[wp]: "\if_unsafe_then_cap' and cte_wp_at' (\c. cteCap c = NullCap) dest and ex_cte_cap_to' dest\ cteInsert cap src dest \\rv s. if_unsafe_then_cap' s\" apply (simp add: ifunsafe'_def3 cteInsert_def setUntypedCapAsFull_def split del: split_if) apply (wp getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of ex_cte_cap_to'_def cteCaps_of_def dest!: modify_map_K_D split: split_if_asm) apply (intro conjI) apply clarsimp apply (erule_tac x = crefa in allE) apply (clarsimp simp:modify_map_def split:split_if_asm) apply (rule_tac x = cref in exI) apply fastforce apply (clarsimp simp:isCap_simps) apply (rule_tac x = cref' in exI) apply fastforce apply (intro conjI impI) apply clarsimp apply (rule_tac x = cref' in exI) apply fastforce apply (clarsimp simp:modify_map_def) apply (erule_tac x = crefa in allE) apply (intro conjI impI) apply clarsimp apply (rule_tac x = cref in exI) apply fastforce apply (clarsimp simp:isCap_simps) apply (rule_tac x = cref' in exI) apply fastforce done lemma setCTE_inQ[wp]: "\\s. P (obj_at' (inQ d p) t s)\ setCTE ptr v \\rv s. P (obj_at' (inQ d p) t s)\" apply (simp add: setCTE_def) apply (rule setObject_cte_obj_at_tcb') apply (simp_all add: inQ_def) done lemma setCTE_valid_queues'[wp]: "\valid_queues'\ setCTE p cte \\rv. valid_queues'\" apply (simp only: valid_queues'_def imp_conv_disj) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift) done crunch inQ[wp]: cteInsert "\s. P (obj_at' (inQ d p) t s)" (wp: crunch_wps) lemma setCTE_it'[wp]: "\\s. P (ksIdleThread s)\ setCTE c p \\_ s. P (ksIdleThread s)\" apply (simp add: setCTE_def setObject_def split_def updateObject_cte) apply (wp|wpc|simp add: unless_def)+ done lemma setCTE_idle [wp]: "\valid_idle'\ setCTE p cte \\rv. valid_idle'\" apply (simp add: valid_idle'_def) apply (rule hoare_lift_Pf [where f="ksIdleThread"]) apply (wp setCTE_pred_tcb_at') done crunch it[wp]: getCTE "\s. P (ksIdleThread s)" lemma getCTE_no_idle_cap: "\valid_global_refs'\ getCTE p \\rv s. ksIdleThread s \ capRange (cteCap rv)\" apply (wp getCTE_wp) apply (clarsimp simp: valid_global_refs'_def valid_refs'_def cte_wp_at_ctes_of) apply blast done lemma updateMDB_idle'[wp]: "\valid_idle'\ updateMDB p m \\rv. valid_idle'\" apply (clarsimp simp add: updateMDB_def) apply (rule hoare_pre) apply (wp | simp add: valid_idle'_def)+ done lemma updateCap_idle': "\valid_idle'\ updateCap p c \\rv. valid_idle'\" apply (simp add: updateCap_def) apply (wp | simp)+ done crunch idle [wp]: setUntypedCapAsFull "valid_idle'" (wp: crunch_wps simp: cte_wp_at_ctes_of) lemma cteInsert_idle'[wp]: "\valid_idle'\ cteInsert cap src dest \\rv. valid_idle'\" apply (simp add: cteInsert_def) apply (wp updateMDB_idle' updateCap_idle' | rule hoare_drop_imp | simp)+ done lemma setCTE_arch [wp]: "\\s. P (ksArchState s)\ setCTE p c \\_ s. P (ksArchState s)\" apply (simp add: setCTE_def setObject_def split_def updateObject_cte) apply (wp|wpc|simp add: unless_def)+ done lemma setCTE_valid_arch[wp]: "\valid_arch_state'\ setCTE p c \\_. valid_arch_state'\" by (wp valid_arch_state_lift' setCTE_typ_at') lemma setCTE_global_refs[wp]: "\\s. P (global_refs' s)\ setCTE p c \\_ s. P (global_refs' s)\" apply (simp add: setCTE_def setObject_def split_def updateObject_cte global_refs'_def) apply (wp|wpc|simp add: unless_def)+ done lemma setCTE_gsMaxObjectSize[wp]: "\\s. P (gsMaxObjectSize s)\ setCTE p c \\_ s. P (gsMaxObjectSize s)\" apply (simp add: setCTE_def setObject_def split_def updateObject_cte) apply (wp|wpc|simp add: unless_def)+ done lemma setCTE_valid_globals[wp]: "\valid_global_refs' and (\s. kernel_data_refs \ capRange (cteCap c) = {}) and (\s. 2 ^ capBits (cteCap c) \ gsMaxObjectSize s)\ setCTE p c \\_. valid_global_refs'\" apply (simp add: valid_global_refs'_def valid_refs'_def pred_conj_def) apply (rule hoare_lift_Pf2 [where f=global_refs']) apply (rule hoare_lift_Pf2 [where f=gsMaxObjectSize]) apply wp apply (clarsimp simp: ran_def valid_cap_sizes'_def) apply metis apply wp done lemma updateMDB_global_refs [wp]: "\valid_global_refs'\ updateMDB p m \\rv. valid_global_refs'\" apply (clarsimp simp add: updateMDB_def) apply (rule hoare_pre) apply (wp getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of valid_global_refs'_def valid_refs'_def valid_cap_sizes'_def) apply blast done lemma updateCap_global_refs [wp]: "\valid_global_refs' and (\s. kernel_data_refs \ capRange cap = {}) and (\s. 2 ^ capBits cap \ gsMaxObjectSize s)\ updateCap p cap \\rv. valid_global_refs'\" apply (clarsimp simp add: updateCap_def) apply (rule hoare_pre) apply (wp getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of) done crunch arch [wp]: cteInsert "\s. P (ksArchState s)" (wp: crunch_wps simp: cte_wp_at_ctes_of) lemma cteInsert_valid_arch [wp]: "\valid_arch_state'\ cteInsert cap src dest \\rv. valid_arch_state'\" by (rule valid_arch_state_lift') wp lemma cteInsert_valid_irq_handlers'[wp]: "\\s. valid_irq_handlers' s \ (\irq. cap = IRQHandlerCap irq \ irq_issued' irq s)\ cteInsert cap src dest \\rv. valid_irq_handlers'\" apply (simp add: valid_irq_handlers'_def cteInsert_def irq_issued'_def setUntypedCapAsFull_def) apply (wp getCTE_wp) apply (clarsimp simp:cte_wp_at_ctes_of) apply (intro conjI impI) apply (clarsimp simp:ran_dom modify_map_dom) apply (drule bspec) apply fastforce apply (clarsimp simp:isCap_simps modify_map_def split:if_splits) apply (clarsimp simp:ran_dom modify_map_dom) apply (drule bspec) apply fastforce apply (clarsimp simp:modify_map_def split:if_splits) done lemma setCTE_valid_mappings'[wp]: "\valid_pde_mappings'\ setCTE x y \\rv. valid_pde_mappings'\" apply (wp valid_pde_mappings_lift' setCTE_typ_at') apply (simp add: setCTE_def) apply (rule obj_at_setObject2) apply (clarsimp simp: updateObject_cte typeError_def in_monad split: Structures_H.kernel_object.split_asm split_if_asm) done crunch pde_mappings' [wp]: cteInsert valid_pde_mappings' (wp: crunch_wps) lemma setCTE_irq_states' [wp]: "\valid_irq_states'\ setCTE x y \\_. valid_irq_states'\" apply (rule valid_irq_states_lift') apply wp apply (simp add: setCTE_def) apply (wp setObject_ksMachine) apply (simp add: updateObject_cte) apply (rule hoare_pre) apply (wp hoare_unless_wp|wpc|simp)+ apply fastforce done crunch irq_states' [wp]: cteInsert valid_irq_states' (wp: crunch_wps) crunch pred_tcb_at'[wp]: cteInsert "pred_tcb_at' proj P t" (wp: crunch_wps) lemma setCTE_cteCaps_of[wp]: "\\s. P ((cteCaps_of s)(p \ cteCap cte))\ setCTE p cte \\rv s. P (cteCaps_of s)\" apply (simp add: cteCaps_of_def) apply wp apply (clarsimp elim!: rsubst[where P=P] intro!: ext) done crunch inQ[wp]: setupReplyMaster "\s. P (obj_at' (inQ d p) t s)" (wp: crunch_wps) crunch norq[wp]: setupReplyMaster "\s. P (ksReadyQueues s)" (wp: crunch_wps) crunch ct[wp]: setupReplyMaster "\s. P (ksCurThread s)" (wp: crunch_wps) crunch state_refs_of'[wp]: setupReplyMaster "\s. P (state_refs_of' s)" (wp: crunch_wps) crunch it[wp]: setupReplyMaster "\s. P (ksIdleThread s)" (wp: setCTE_it') crunch nosch[wp]: setupReplyMaster "\s. P (ksSchedulerAction s)" crunch irq_node'[wp]: setupReplyMaster "\s. P (irq_node' s)" (ignore: updateObject) lemmas setCTE_cteCap_wp_irq[wp] = hoare_use_eq_irq_node' [OF setCTE_irq_node' setCTE_cteCaps_of] crunch global_refs'[wp]: setUntypedCapAsFull "\s. P (global_refs' s) " (simp: crunch_simps) lemma setUntypedCapAsFull_valid_refs'[wp]: "\\s. valid_refs' R (ctes_of s) \ cte_wp_at' (op = srcCTE) src s\ setUntypedCapAsFull (cteCap srcCTE) cap src \\yb s. valid_refs' R (ctes_of s)\" apply (clarsimp simp:valid_refs'_def setUntypedCapAsFull_def split del:if_splits) apply (rule hoare_pre) apply (wp updateCap_ctes_of_wp) apply (clarsimp simp:ran_dom) apply (drule_tac x = y in bspec) apply (drule_tac a = y in domI) apply (simp add:modify_map_dom) apply (clarsimp simp:modify_map_def cte_wp_at_ctes_of isCap_simps split:if_splits) done crunch gsMaxObjectSize[wp]: setUntypedCapAsFull "\s. P (gsMaxObjectSize s)" lemma setUntypedCapAsFull_sizes[wp]: "\\s. valid_cap_sizes' sz (ctes_of s) \ cte_wp_at' (op = srcCTE) src s\ setUntypedCapAsFull (cteCap srcCTE) cap src \\rv s. valid_cap_sizes' sz (ctes_of s)\" apply (clarsimp simp:valid_cap_sizes'_def setUntypedCapAsFull_def split del:if_splits) apply (rule hoare_pre) apply (wp updateCap_ctes_of_wp | wps)+ apply (clarsimp simp:ran_dom) apply (drule_tac x = y in bspec) apply (drule_tac a = y in domI) apply (simp add:modify_map_dom) apply (clarsimp simp:modify_map_def cte_wp_at_ctes_of isCap_simps split:if_splits) done lemma setUntypedCapAsFull_valid_global_refs'[wp]: "\\s. valid_global_refs' s \ cte_wp_at' (op = srcCTE) src s\ setUntypedCapAsFull (cteCap srcCTE) cap src \\yb s. valid_global_refs' s\" apply (clarsimp simp: valid_global_refs'_def) apply (rule hoare_pre,wps) apply wp apply simp done lemma capMaster_eq_capBits_eq: "capMasterCap cap = capMasterCap cap' \ capBits cap = capBits cap'" by (metis capBits_Master) lemma valid_global_refsD_with_objSize: "\ ctes_of s p = Some cte; valid_global_refs' s \ \ kernel_data_refs \ capRange (cteCap cte) = {} \ global_refs' s \ kernel_data_refs \ 2 ^ capBits (cteCap cte) \ gsMaxObjectSize s" by (clarsimp simp: valid_global_refs'_def valid_refs'_def valid_cap_sizes'_def ran_def) blast lemma cteInsert_valid_globals [wp]: "\valid_global_refs' and (\s. cte_wp_at' (is_derived' (ctes_of s) src cap \ cteCap) src s)\ cteInsert cap src dest \\rv. valid_global_refs'\" apply (simp add: cteInsert_def) apply (rule hoare_pre) apply (wp getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of is_derived'_def badge_derived'_def) apply (frule capMaster_eq_capBits_eq) apply (drule capMaster_capRange) apply (drule (1) valid_global_refsD_with_objSize) apply simp done crunch arch [wp]: cteInsert "\s. P (ksArchState s)" (wp: crunch_wps simp: cte_wp_at_ctes_of) crunch pde_mappings' [wp]: cteInsert valid_pde_mappings' (wp: crunch_wps) lemma setCTE_ksMachine[wp]: "\\s. P (ksMachineState s)\ setCTE x y \\_ s. P (ksMachineState s)\" apply (clarsimp simp: setCTE_def) apply (wp setObject_ksMachine) apply (clarsimp simp: updateObject_cte split: Structures_H.kernel_object.splits) apply (safe, (wp hoare_unless_wp | simp)+) done crunch ksMachine[wp]: cteInsert "\s. P (ksMachineState s)" (wp: crunch_wps) lemma cteInsert_vms'[wp]: "\valid_machine_state'\ cteInsert cap src dest \\rv. valid_machine_state'\" apply (simp add: cteInsert_def valid_machine_state'_def pointerInUserData_def) apply (intro hoare_vcg_all_lift hoare_vcg_disj_lift) apply (wp setObject_typ_at_inv setObject_ksMachine updateObject_default_inv | intro hoare_drop_imp)+ done crunch pspace_domain_valid[wp]: cteInsert "pspace_domain_valid" (wp: crunch_wps) lemma setCTE_ct_not_inQ[wp]: "\ct_not_inQ\ setCTE ptr cte \\_. ct_not_inQ\" apply (rule ct_not_inQ_lift [OF setCTE_nosch]) apply (simp add: setCTE_def ct_not_inQ_def) apply (rule hoare_weaken_pre) apply (wps setObject_cte_ct) apply (rule setObject_cte_obj_at_tcb') apply (clarsimp simp add: obj_at'_def)+ done crunch ct_not_inQ[wp]: cteInsert "ct_not_inQ" (simp: crunch_simps wp: hoare_drop_imp) lemma setCTE_ksCurDomain[wp]: "\\s. P (ksCurDomain s)\ setCTE p cte \\rv s. P (ksCurDomain s)\" apply (simp add: setCTE_def) apply wp done lemma setObject_cte_ksDomSchedule[wp]: "\ \s. P (ksDomSchedule s) \ setObject ptr (v::cte) \ \_ s. P (ksDomSchedule s) \" apply (simp add: setObject_def split_def) apply (wp updateObject_cte_inv | simp)+ done lemma setCTE_ksDomSchedule[wp]: "\\s. P (ksDomSchedule s)\ setCTE p cte \\rv s. P (ksDomSchedule s)\" apply (simp add: setCTE_def) apply wp done crunch ksCurDomain[wp]: cteInsert "\s. P (ksCurDomain s)" (wp: crunch_wps ) crunch ksIdleThread[wp]: cteInsert "\s. P (ksIdleThread s)" (wp: crunch_wps) crunch ksDomSchedule[wp]: cteInsert "\s. P (ksDomSchedule s)" (wp: crunch_wps) lemma setCTE_tcbDomain_inv[wp]: "\obj_at' (\tcb. P (tcbDomain tcb)) t\ setCTE ptr v \\_. obj_at' (\tcb. P (tcbDomain tcb)) t\" apply (simp add: setCTE_def) apply (rule setObject_cte_obj_at_tcb', simp_all) done crunch tcbDomain_inv[wp]: cteInsert "obj_at' (\tcb. P (tcbDomain tcb)) t" (wp: crunch_simps hoare_drop_imps) lemma setCTE_tcbPriority_inv[wp]: "\obj_at' (\tcb. P (tcbPriority tcb)) t\ setCTE ptr v \\_. obj_at' (\tcb. P (tcbPriority tcb)) t\" apply (simp add: setCTE_def) apply (rule setObject_cte_obj_at_tcb', simp_all) done crunch tcbPriority_inv[wp]: cteInsert "obj_at' (\tcb. P (tcbPriority tcb)) t" (wp: crunch_simps hoare_drop_imps) lemma cteInsert_ct_idle_or_in_cur_domain'[wp]: "\ ct_idle_or_in_cur_domain' \ cteInsert a b c \ \_. ct_idle_or_in_cur_domain' \" apply (rule ct_idle_or_in_cur_domain'_lift) apply (wp hoare_vcg_disj_lift) done lemma setObject_cte_domIdx: "\\s. P (ksDomScheduleIdx s)\ setObject t (v::cte) \\rv s. P (ksDomScheduleIdx s)\" by (clarsimp simp: valid_def setCTE_def[symmetric] dest!: setCTE_pspace_only) crunch ksDomScheduleIdx[wp]: cteInsert "\s. P (ksDomScheduleIdx s)" (wp: setObject_cte_domIdx hoare_drop_imps ignore: setObject) lemma cteInsert_invs: "\invs' and cte_wp_at' (\c. cteCap c=NullCap) dest and valid_cap' cap and (\s. src \ dest) and (\s. cte_wp_at' (is_derived' (ctes_of s) src cap \ cteCap) src s) and ex_cte_cap_to' dest and (\s. \irq. cap = IRQHandlerCap irq \ irq_issued' irq s)\ cteInsert cap src dest \\rv. invs'\" apply (rule hoare_pre) apply (simp add: invs'_def valid_state'_def valid_pspace'_def) apply (wp cur_tcb_lift tcb_in_cur_domain'_lift sch_act_wf_lift valid_irq_node_lift valid_queues_lift' irqs_masked_lift cteInsert_norq | simp add: st_tcb_at'_def)+ apply (wp cur_tcb_lift tcb_in_cur_domain'_lift sch_act_wf_lift CSpace_R.valid_queues_lift valid_irq_node_lift valid_queues_lift' irqs_masked_lift cteInsert_norq | simp add: pred_tcb_at'_def)+ apply (auto simp: invs'_def valid_state'_def valid_pspace'_def elim: valid_capAligned) done lemma derive_cap_corres: "\cap_relation c c'; cte = cte_map slot \ \ corres (ser \ cap_relation) (cte_at slot) (pspace_aligned' and pspace_distinct' and cte_at' cte and valid_mdb') (derive_cap slot c) (deriveCap cte c')" apply (unfold derive_cap_def deriveCap_def) apply (case_tac c) apply (simp_all add: returnOk_def Let_def is_zombie_def isCap_simps split: sum.splits) apply (rule corres_initial_splitE [OF ensure_no_children_corres]) apply simp apply clarsimp apply wp apply clarsimp apply (rule corres_rel_imp) apply (rule corres_guard_imp) apply (rule arch_derive_corres) apply (clarsimp simp: o_def)+ done lemma deriveCap_inv[wp]: "\P\ deriveCap cte c \\rv. P\" apply (case_tac c, simp_all add: deriveCap_def ensureNoChildren_def whenE_def isCap_simps Let_def, wp) apply clarsimp apply (wp arch_deriveCap_inv | simp)+ done lemma lookup_cap_valid': "\valid_objs'\ lookupCap t c \valid_cap'\, -" apply (simp add: lookupCap_def lookupCapAndSlot_def lookupSlotForThread_def split_def) apply (wp | simp)+ done lemma capAligned_Null [simp]: "capAligned NullCap" by (simp add: capAligned_def is_aligned_def word_bits_def) lemma guarded_lookup_valid_cap': "\ valid_objs' \ nullCapOnFailure (lookupCap t c) \\rv. valid_cap' rv \" apply (simp add: nullCapOnFailure_def) apply wp apply (simp add: valid_cap'_def) apply (fold validE_R_def) apply (rule lookup_cap_valid') done lemma setObject_tcb_tcb': "\tcb_at' p\ setObject p (t::tcb) \\rv. tcb_at' p\" apply (rule obj_at_setObject1) apply (simp add: updateObject_default_def in_monad) apply (simp add: projectKOs) apply (simp add: objBits_simps) done lemma cte_wp_at'_conjI: "\ cte_wp_at' P p s; cte_wp_at' Q p s \ \ cte_wp_at' (\c. P c \ Q c) p s" by (auto simp add: cte_wp_at'_def) crunch inv'[wp]: rangeCheck "P" (simp: crunch_simps) lemma lookupSlotForCNodeOp_inv'[wp]: "\P\ lookupSlotForCNodeOp src root ptr depth \\rv. P\" apply (simp add: lookupSlotForCNodeOp_def split_def unlessE_def cong: if_cong split del: split_if) apply (rule hoare_pre) apply (wp hoare_drop_imps) apply simp done lemma unifyFailure_inv [wp]: "\P\ f \\_. P\, \\_. P\ \ \P\ unifyFailure f \\_. P\, \\_. P\" unfolding unifyFailure_def apply (simp add: rethrowFailure_def const_def o_def) apply wp apply simp done (* FIXME: move *) lemma loadWordUser_inv [wp]: "\P\ loadWordUser p \\rv. P\" unfolding loadWordUser_def by (wp dmo_inv' loadWord_inv) lemma capTransferFromWords_inv: "\P\ capTransferFromWords buffer \\_. P\" apply (simp add: capTransferFromWords_def) apply wp done lemma lct_inv' [wp]: "\P\ loadCapTransfer b \\rv. P\" unfolding loadCapTransfer_def apply (wp capTransferFromWords_inv) done lemma maskCapRightsNull [simp]: "maskCapRights R NullCap = NullCap" by (simp add: maskCapRights_def isCap_defs) lemma maskCapRightsUntyped [simp]: "maskCapRights R (UntypedCap r n f) = UntypedCap r n f" by (simp add: maskCapRights_def isCap_defs Let_def) lemma maskCapRightsZombie [simp]: "maskCapRights R (Zombie p b n) = Zombie p b n" by (simp add: maskCapRights_def isCap_defs Let_def) (* FIXME: move *) lemma cap_relation_update_masks: "cap_relation a c' \ cap_relation (cap_rights_update (cap_rights a - {AllowWrite}) a) (maskCapRights (capAllowWrite_update (\_. False) allRights) c')" apply (drule_tac rmask="UNIV - {AllowWrite}" in cap_relation_masks) by (simp add: rights_mask_map_def allRights_def) declare if_option_Some[simp] lemma lookup_cap_corres: "\ epcptr = to_bl epcptr' \ \ corres (lfr \ cap_relation) (valid_objs and pspace_aligned and tcb_at thread) (valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' thread) (lookup_cap thread epcptr) (lookupCap thread epcptr')" apply (simp add: lookup_cap_def lookupCap_def lookupCapAndSlot_def) apply (rule corres_guard_imp) apply (rule corres_splitEE [OF _ lookup_slot_corres]) apply (simp add: split_def) apply (subst bindE_returnOk[symmetric]) apply (rule corres_splitEE) prefer 2 apply simp apply (rule getSlotCap_corres, rule refl) apply (rule corres_returnOk [of _ \ \]) apply simp apply wp apply auto done lemma ensureNoChildren_inv[wp]: "\P\ ensureNoChildren ptr \\rv. P\" apply (simp add: ensureNoChildren_def whenE_def) apply (wp hoare_drop_imps) apply auto done lemma ensure_empty_corres: "q = cte_map p \ corres (ser \ dc) (invs and cte_at p) invs' (ensure_empty p) (ensureEmptySlot q)" apply (clarsimp simp add: ensure_empty_def ensureEmptySlot_def unlessE_whenE liftE_bindE) apply (rule corres_guard_imp) apply (rule corres_split [OF _ get_cap_corres]) apply (rule corres_trivial) apply (case_tac cap, auto simp add: whenE_def returnOk_def)[1] apply wp apply (clarsimp simp: invs_valid_objs invs_psp_aligned) apply fastforce done lemma ensureEmpty_inv[wp]: "\P\ ensureEmptySlot p \\rv. P\" by (simp add: ensureEmptySlot_def unlessE_whenE whenE_def | wp)+ lemma lsfc_corres: "\cap_relation c c'; ptr = to_bl ptr'\ \ corres (ser \ (\cref cref'. cref' = cte_map cref)) (valid_objs and pspace_aligned and valid_cap c) (valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' c') (lookup_slot_for_cnode_op s c ptr depth) (lookupSlotForCNodeOp s c' ptr' depth)" apply (simp add: lookup_slot_for_cnode_op_def lookupSlotForCNodeOp_def) apply (clarsimp simp: lookup_failure_map_def split_def word_size) apply (clarsimp simp: rangeCheck_def[unfolded fun_app_def unlessE_def] whenE_def word_bits_def toInteger_nat fromIntegral_def fromInteger_nat) apply (rule corres_lookup_error) apply (rule corres_guard_imp) apply (rule corres_splitEE [OF _ rab_corres']) apply (rule corres_trivial) apply (clarsimp simp: returnOk_def lookup_failure_map_def split: list.split) apply simp+ apply wp apply clarsimp apply clarsimp done (* this helper characterisation of ctes_of is needed in CNodeInv and Untyped *) lemma ensureNoChildren_wp: "\\s. Q s \ (descendants_of' p (ctes_of s) = {} \ P () s)\ ensureNoChildren p \P\,\\_. Q\" apply (simp add: ensureNoChildren_def whenE_def) apply (wp getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def descendants_of'_def) apply (rule conjI) apply clarsimp apply (erule (4) subtree_no_parent) apply clarsimp apply (erule (2) subtree_next_0) done lemma set_cap_pspace_corres: "cap_relation cap (cteCap cte) \ corres_underlying {(s, s'). pspace_relations (ekheap (s)) (kheap s) (ksPSpace s')} True dc (pspace_distinct and pspace_aligned and valid_objs and cte_at p) (pspace_aligned' and pspace_distinct' and cte_at' (cte_map p)) (set_cap cap p) (setCTE (cte_map p) cte)" apply (rule corres_no_failI) apply (rule no_fail_pre, wp) apply simp apply clarsimp apply (drule(8) set_cap_not_quite_corres_prequel) apply simp apply fastforce done (* FIXME: move to StateRelation *) lemma ghost_relation_of_heap: "ghost_relation h ups cns \ ups_of_heap h = ups \ cns_of_heap h = cns" apply (rule iffI) apply (rule conjI) apply (rule ext) apply (clarsimp simp add: ghost_relation_def ups_of_heap_def) apply (drule_tac x=x in spec) apply (auto simp add: ghost_relation_def ups_of_heap_def split: option.splits Structures_A.kernel_object.splits arch_kernel_obj.splits)[1] apply (rule ext) apply (clarsimp simp add: ghost_relation_def cns_of_heap_def) apply (drule_tac x=x in spec)+ apply (rule ccontr) apply (simp split: option.splits Structures_A.kernel_object.splits arch_kernel_obj.splits)[1] apply (simp split: split_if_asm) apply force apply (drule not_sym) apply clarsimp apply (erule_tac x=y in allE) apply simp apply (auto simp add: ghost_relation_def ups_of_heap_def cns_of_heap_def split: option.splits Structures_A.kernel_object.splits arch_kernel_obj.splits split_if_asm) done lemma corres_caps_decomposition: assumes x: "corres_underlying {(s, s'). pspace_relations (ekheap (s)) (kheap s) (ksPSpace s')} True r P P' f g" assumes u: "\P. \\s. P (new_caps s)\ f \\rv s. P (caps_of_state s)\" "\P. \\s. P (new_mdb s)\ f \\rv s. P (cdt s)\" "\P. \\s. P (new_list s)\ f \\rv s. P (cdt_list (s))\" "\P. \\s. P (new_rvk s)\ f \\rv s. P (is_original_cap s)\" "\P. \\s. P (new_ctes s)\ g \\rv s. P (ctes_of s)\" "\P. \\s. P (new_ms s)\ f \\rv s. P (machine_state s)\" "\P. \\s. P (new_ms' s)\ g \\rv s. P (ksMachineState s)\" "\P. \\s. P (new_wuc s)\ f \\rv s. P (work_units_completed s)\" "\P. \\s. P (new_wuc' s)\ g \\rv s. P (ksWorkUnitsCompleted s)\" "\P. \\s. P (new_ct s)\ f \\rv s. P (cur_thread s)\" "\P. \\s. P (new_ct' s)\ g \\rv s. P (ksCurThread s)\" "\P. \\s. P (new_as s)\ f \\rv s. P (arch_state s)\" "\P. \\s. P (new_as' s)\ g \\rv s. P (ksArchState s)\" "\P. \\s. P (new_id s)\ f \\rv s. P (idle_thread s)\" "\P. \\s. P (new_id' s)\ g \\rv s. P (ksIdleThread s)\" "\P. \\s. P (new_irqn s)\ f \\rv s. P (interrupt_irq_node s)\" "\P. \\s. P (new_irqs s)\ f \\rv s. P (interrupt_states s)\" "\P. \\s. P (new_irqs' s)\ g \\rv s. P (ksInterruptState s)\" "\P. \\s. P (new_ups s)\ f \\rv s. P (ups_of_heap (kheap s))\" "\P. \\s. P (new_ups' s)\ g \\rv s. P (gsUserPages s)\" "\P. \\s. P (new_cns s)\ f \\rv s. P (cns_of_heap (kheap s))\" "\P. \\s. P (new_cns' s)\ g \\rv s. P (gsCNodes s)\" "\P. \\s. P (new_queues s)\ f \\rv s. P (ready_queues s)\" "\P. \\s. P (new_action s)\ f \\rv s. P (scheduler_action s)\" "\P. \\s. P (new_sa' s)\ g \\rv s. P (ksSchedulerAction s)\" "\P. \\s. P (new_rqs' s)\ g \\rv s. P (ksReadyQueues s)\" "\P. \\s. P (new_di s)\ f \\rv s. P (domain_index s)\" "\P. \\s. P (new_dl s)\ f \\rv s. P (domain_list s)\" "\P. \\s. P (new_cd s)\ f \\rv s. P (cur_domain s)\" "\P. \\s. P (new_dt s)\ f \\rv s. P (domain_time s)\" "\P. \\s. P (new_dsi' s)\ g \\rv s. P (ksDomScheduleIdx s)\" "\P. \\s. P (new_ds' s)\ g \\rv s. P (ksDomSchedule s)\" "\P. \\s. P (new_cd' s)\ g \\rv s. P (ksCurDomain s)\" "\P. \\s. P (new_dt' s)\ g \\rv s. P (ksDomainTime s)\" assumes z: "\s s'. \ P s; P' s'; (s, s') \ state_relation \ \ cdt_relation (op \ None \ new_caps s) (new_mdb s) (new_ctes s')" "\s s'. \ P s; P' s'; (s, s') \ state_relation \ \ cdt_list_relation (new_list s) (new_mdb s) (new_ctes s')" "\s s'. \ P s; P' s'; (s, s') \ state_relation \ \ sched_act_relation (new_action s) (new_sa' s')" "\s s'. \ P s; P' s'; (s, s') \ state_relation \ \ ready_queues_relation (new_queues s) (new_rqs' s')" "\s s'. \ P s; P' s'; (s, s') \ state_relation \ \ revokable_relation (new_rvk s) (null_filter (new_caps s)) (new_ctes s')" "\s s'. \ P s; P' s'; (s, s') \ state_relation \ \ (new_as s, new_as' s') \ arch_state_relation \ interrupt_state_relation (new_irqn s) (new_irqs s) (new_irqs' s') \ new_ct s = new_ct' s' \ new_id s = new_id' s' \ new_ms s = new_ms' s' \ new_di s = new_dsi' s' \ new_dl s = new_ds' s' \ new_cd s = new_cd' s' \ new_dt s = new_dt' s' \ new_wuc s = new_wuc' s'" "\s s'. \ P s; P' s'; (s, s') \ state_relation \ \ new_ups s = new_ups' s'" "\s s'. \ P s; P' s'; (s, s') \ state_relation \ \ new_cns s = new_cns' s'" shows "corres r P P' f g" proof - have all_ext: "\f f'. (\p. f p = f' p) = (f = f')" by (fastforce intro!: ext) have mdb_wp': "\ctes. \\s. cdt_relation (op \ None \ new_caps s) (new_mdb s) ctes\ f \\rv s. \m ca. (\p. ca p = (op \ None \ caps_of_state s) p) \ m = cdt s \ cdt_relation ca m ctes\" apply (wp hoare_vcg_ex_lift hoare_vcg_all_lift u) apply (subst all_ext) apply (simp add: o_def) done note mdb_wp = mdb_wp' [simplified all_ext simp_thms] have list_wp': "\ctes. \\s. cdt_list_relation (new_list s) (new_mdb s) ctes\ f \\rv s. \m t. t = cdt_list s \ m = cdt s \ cdt_list_relation t m ctes\" apply (wp hoare_vcg_ex_lift hoare_vcg_all_lift u) apply (simp add: o_def) done note list_wp = list_wp' [simplified all_ext simp_thms] have rvk_wp': "\ctes. \\s. revokable_relation (new_rvk s) (null_filter (new_caps s)) ctes\ f \\rv s. revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) ctes\" unfolding revokable_relation_def apply (simp only: imp_conv_disj) apply (wp hoare_vcg_ex_lift hoare_vcg_all_lift hoare_vcg_disj_lift u) done have exs_wp': "\ctes. \\s. revokable_relation (new_rvk s) (null_filter (new_caps s)) ctes\ f \\rv s. revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) ctes\" unfolding revokable_relation_def apply (simp only: imp_conv_disj) apply (wp hoare_vcg_ex_lift hoare_vcg_all_lift hoare_vcg_disj_lift u) done note rvk_wp = rvk_wp' [simplified all_ext simp_thms] have swp_cte_at: "\s. swp cte_at s = (op \ None \ caps_of_state s)" by (rule ext, simp, subst neq_commute, simp add: cte_wp_at_caps_of_state) have abs_irq_together': "\P. \\s. P (new_irqn s) (new_irqs s)\ f \\rv s. \irn. interrupt_irq_node s = irn \ P irn (interrupt_states s)\" by (wp hoare_vcg_ex_lift u, simp) note abs_irq_together = abs_irq_together'[simplified] show ?thesis unfolding state_relation_def swp_cte_at apply (subst conj_assoc[symmetric]) apply (subst pspace_relations_def[symmetric]) apply (rule corres_underlying_decomposition [OF x]) apply (simp add: ghost_relation_of_heap) apply (wp hoare_vcg_conj_lift mdb_wp rvk_wp list_wp u abs_irq_together) apply (intro z[simplified o_def] conjI | simp add: state_relation_def pspace_relations_def swp_cte_at | (clarsimp, drule (1) z(6), simp add: state_relation_def pspace_relations_def swp_cte_at))+ done qed lemma getCTE_symb_exec_r: "corres_underlying sr nf dc \ (cte_at' p) (return ()) (getCTE p)" apply (rule corres_no_failI, wp) apply (clarsimp simp: return_def elim!: use_valid [OF _ getCTE_inv]) done lemma updateMDB_symb_exec_r: "corres_underlying {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} nf dc \ (pspace_aligned' and pspace_distinct' and (no_0 \ ctes_of) and (\s. p \ 0 \ cte_at' p s)) (return ()) (updateMDB p m)" using no_fail_updateMDB [of p m] apply (clarsimp simp: corres_underlying_def return_def no_fail_def) apply (drule(1) updateMDB_the_lot, simp, assumption+) apply clarsimp done lemma updateMDB_ctes_of_cases: "\\s. P (modify_map (ctes_of s) p (if p = 0 then id else cteMDBNode_update f))\ updateMDB p f \\rv s. P (ctes_of s)\" apply (simp add: updateMDB_def split del: split_if) apply (rule hoare_pre, wp getCTE_ctes_of) apply (clarsimp simp: modify_map_def map_option_case split: option.split | rule conjI ext | erule rsubst[where P=P])+ apply (case_tac y, simp) done crunch ct[wp]: updateMDB "\s. P (ksCurThread s)" lemma setCTE_state_bits[wp]: "\\s. P (ksMachineState s)\ setCTE p v \\rv s. P (ksMachineState s)\" "\\s. Q (ksIdleThread s)\ setCTE p v \\rv s. Q (ksIdleThread s)\" "\\s. R (ksArchState s)\ setCTE p v \\rv s. R (ksArchState s)\" "\\s. S (ksInterruptState s)\ setCTE p v \\rv s. S (ksInterruptState s)\" apply (simp_all add: setCTE_def setObject_def split_def) apply (wp updateObject_cte_inv | simp)+ done crunch ms'[wp]: updateMDB "\s. P (ksMachineState s)" crunch idle'[wp]: updateMDB "\s. P (ksIdleThread s)" crunch arch'[wp]: updateMDB "\s. P (ksArchState s)" crunch int'[wp]: updateMDB "\s. P (ksInterruptState s)" lemma cte_map_eq_subst: "\ cte_at p s; cte_at p' s; valid_objs s; pspace_aligned s; pspace_distinct s \ \ (cte_map p = cte_map p') = (p = p')" by (fastforce elim!: cte_map_inj_eq) lemma revokable_relation_simp: "\ (s, s') \ state_relation; null_filter (caps_of_state s) p = Some c; ctes_of s' (cte_map p) = Some (CTE cap node) \ \ mdbRevocable node = is_original_cap s p" by (cases p, clarsimp simp: state_relation_def revokable_relation_def) lemma setCTE_gsUserPages[wp]: "\\s. P (gsUserPages s)\ setCTE p v \\rv s. P (gsUserPages s)\" apply (simp add: setCTE_def setObject_def split_def) apply (wp updateObject_cte_inv crunch_wps | simp)+ done lemma setCTE_gsCNodes[wp]: "\\s. P (gsCNodes s)\ setCTE p v \\rv s. P (gsCNodes s)\" apply (simp add: setCTE_def setObject_def split_def) apply (wp updateObject_cte_inv crunch_wps | simp)+ done lemma set_original_symb_exec_l': "corres_underlying {(s, s'). f (ekheap s) (kheap s) s'} nf dc P P' (set_original p b) (return x)" by (simp add: corres_underlying_def return_def set_original_def in_monad Bex_def) lemma setCTE_schedule_index[wp]: "\\s. P (ksDomScheduleIdx s)\ setCTE p v \\rv s. P (ksDomScheduleIdx s)\" apply (simp add: setCTE_def setObject_def split_def) apply (wp updateObject_cte_inv crunch_wps | simp)+ done lemma setCTE_schedule[wp]: "\\s. P (ksDomSchedule s)\ setCTE p v \\rv s. P (ksDomSchedule s)\" apply (simp add: setCTE_def setObject_def split_def) apply (wp updateObject_cte_inv crunch_wps | simp)+ done lemma setCTE_domain_time[wp]: "\\s. P (ksDomainTime s)\ setCTE p v \\rv s. P (ksDomainTime s)\" apply (simp add: setCTE_def setObject_def split_def) apply (wp updateObject_cte_inv crunch_wps | simp)+ done lemma setCTE_work_units_completed[wp]: "\\s. P (ksWorkUnitsCompleted s)\ setCTE p v \\_ s. P (ksWorkUnitsCompleted s)\" apply (simp add: setCTE_def setObject_def split_def) apply (wp updateObject_cte_inv crunch_wps | simp)+ done lemma create_reply_master_corres: "sl' = cte_map sl \ corres dc (cte_wp_at (op = cap.NullCap) sl and valid_pspace and valid_mdb and valid_list) (cte_wp_at' (\c. cteCap c = NullCap \ mdbPrev (cteMDBNode c) = 0) sl' and valid_mdb' and valid_pspace') (do y \ set_original sl True; set_cap (cap.ReplyCap thread True) sl od) (setCTE sl' (CTE (capability.ReplyCap thread True) initMDBNode))" apply clarsimp apply (rule corres_caps_decomposition) defer apply (wp|simp)+ apply (clarsimp simp: o_def cdt_relation_def cte_wp_at_ctes_of split del: split_if cong: if_cong simp del: id_apply) apply (case_tac cte, clarsimp) apply (fold fun_upd_def) apply (subst descendants_of_Null_update') apply fastforce apply fastforce apply assumption apply assumption apply (simp add: nullPointer_def) apply (subgoal_tac "cte_at (a, b) s") prefer 2 apply (drule not_sym, clarsimp simp: cte_wp_at_caps_of_state split: split_if_asm) apply (simp add: state_relation_def cdt_relation_def) apply (clarsimp simp: o_def cdt_list_relation_def cte_wp_at_ctes_of split del: split_if cong: if_cong simp del: id_apply) apply (case_tac cte, clarsimp) apply (clarsimp simp: state_relation_def cdt_list_relation_def) apply (simp split: split_if_asm) apply (erule_tac x=a in allE, erule_tac x=b in allE) apply clarsimp apply(case_tac "next_slot (a, b) (cdt_list s) (cdt s)") apply(simp) apply(simp) apply(fastforce simp: valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) apply (clarsimp simp: state_relation_def) apply (clarsimp simp: state_relation_def) apply (clarsimp simp add: revokable_relation_def cte_wp_at_ctes_of split del: split_if) apply simp apply (rule conjI) apply (clarsimp simp: initMDBNode_def) apply clarsimp apply (subgoal_tac "null_filter (caps_of_state s) (a, b) \ None") prefer 2 apply (clarsimp simp: null_filter_def cte_wp_at_caps_of_state split: split_if_asm) apply (subgoal_tac "cte_at (a,b) s") prefer 2 apply clarsimp apply (drule null_filter_caps_of_stateD) apply (erule cte_wp_cte_at) apply (clarsimp split: split_if_asm cong: conj_cong simp: cte_map_eq_subst revokable_relation_simp cte_wp_at_cte_at valid_pspace_def) apply (clarsimp simp: state_relation_def) apply (clarsimp elim!: state_relationE simp: ghost_relation_of_heap)+ apply (rule corres_guard_imp) apply (rule corres_underlying_symb_exec_l [OF set_original_symb_exec_l']) apply (rule set_cap_pspace_corres) apply simp apply wp apply (clarsimp simp: cte_wp_at_cte_at valid_pspace_def) apply (clarsimp simp: valid_pspace'_def cte_wp_at'_def) done lemma cte_map_nat_to_cref: "\ n < 2 ^ b; b < 32 \ \ cte_map (p, nat_to_cref b n) = p + (of_nat n * 16)" apply (clarsimp simp: cte_map_def nat_to_cref_def dest!: less_is_drop_replicate) apply (rule arg_cong [where f="\x. x * 16"]) apply (subst of_drop_to_bl) apply (simp add: word_bits_def) apply (subst mask_eq_iff_w2p) apply (simp add: word_size) apply (simp add: word_less_nat_alt word_size word_bits_def) apply (rule order_le_less_trans) defer apply assumption apply (subst unat_of_nat) apply (rule mod_le_dividend) done lemma valid_nullcapsE: "\ valid_nullcaps m; m p = Some (CTE NullCap n); \ mdbPrev n = 0; mdbNext n = 0 \ \ P \ \ P" by (fastforce simp: valid_nullcaps_def nullMDBNode_def nullPointer_def) lemma valid_nullcaps_prev: "\ m (mdbPrev n) = Some (CTE NullCap n'); m p = Some (CTE c n); no_0 m; valid_dlist m; valid_nullcaps m \ \ False" apply (erule (1) valid_nullcapsE) apply (erule_tac p=p in valid_dlistEp, assumption) apply clarsimp apply clarsimp done lemma valid_nullcaps_next: "\ m (mdbNext n) = Some (CTE NullCap n'); m p = Some (CTE c n); no_0 m; valid_dlist m; valid_nullcaps m \ \ False" apply (erule (1) valid_nullcapsE) apply (erule_tac p=p in valid_dlistEn, assumption) apply clarsimp apply clarsimp done defs noReplyCapsFor_def: "noReplyCapsFor \ \t s. \sl m. \ cte_wp_at' (\cte. cteCap cte = ReplyCap t m) sl s" lemma pspace_relation_no_reply_caps: assumes pspace: "pspace_relation (kheap s) (ksPSpace s')" and invs: "invs s" and tcb: "tcb_at t s" and m_cte': "cte_wp_at' (op = cte) sl' s'" and m_null: "cteCap cte = capability.NullCap" and m_sl: "sl' = cte_map (t, tcb_cnode_index 2)" shows "noReplyCapsFor t s'" proof - from tcb have m_cte: "cte_at (t, tcb_cnode_index 2) s" by (clarsimp elim!: tcb_at_cte_at) have m_cte_null: "cte_wp_at (\c. c = cap.NullCap) (t, tcb_cnode_index 2) s" using pspace invs apply (frule_tac pspace_relation_cte_wp_atI') apply (rule assms) apply clarsimp apply (clarsimp simp: m_sl) apply (frule cte_map_inj_eq) apply (rule m_cte) apply (erule cte_wp_cte_at) apply clarsimp+ apply (clarsimp elim!: cte_wp_at_weakenE simp: m_null) done have no_reply_caps: "\sl m. \ cte_wp_at (\c. c = cap.ReplyCap t m) sl s" by (rule no_reply_caps_for_thread [OF invs tcb m_cte_null]) hence noReplyCaps: "\sl m. \ cte_wp_at' (\cte. cteCap cte = ReplyCap t m) sl 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 [OF pspace _ invs_valid_objs [OF invs]]) 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 thus ?thesis by (simp add: noReplyCapsFor_def) qed lemma setup_reply_master_corres: "corres dc (einvs and tcb_at t) (invs' and tcb_at' t) (setup_reply_master t) (setupReplyMaster t)" apply (simp add: setupReplyMaster_def setup_reply_master_def) apply (simp add: locateSlot_conv tcbReplySlot_def objBits_def objBitsKO_def) apply (simp add: nullMDBNode_def, fold initMDBNode_def) apply (rule_tac F="t + 0x20 = cte_map (t, tcb_cnode_index 2)" in corres_req) apply (clarsimp simp: tcb_cnode_index_def2 cte_map_nat_to_cref) apply (clarsimp simp: cte_level_bits_def) apply (rule stronger_corres_guard_imp) apply (rule corres_split [OF _ get_cap_corres]) apply (rule corres_when) apply fastforce apply (rule_tac P'="einvs and tcb_at t" in corres_stateAssert_implied) apply (rule create_reply_master_corres) apply simp apply (subgoal_tac "\cte. cte_wp_at' (op = cte) (cte_map (t, tcb_cnode_index 2)) s' \ cteCap cte = capability.NullCap") apply (fastforce dest: pspace_relation_no_reply_caps state_relation_pspace_relation) apply (clarsimp simp: cte_map_def tcb_cnode_index_def cte_wp_at_ctes_of) apply (rule_tac Q="\rv. einvs and tcb_at t and cte_wp_at (op = rv) (t, tcb_cnode_index 2)" in hoare_strengthen_post) apply (wp hoare_drop_imps get_cap_wp) apply (clarsimp simp: invs_def valid_state_def elim!: cte_wp_at_weakenE) apply (rule_tac Q="\rv. valid_pspace' and valid_mdb' and cte_wp_at' (op = rv) (cte_map (t, tcb_cnode_index 2))" in hoare_strengthen_post) apply (wp hoare_drop_imps getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def) apply (case_tac r, fastforce elim: valid_nullcapsE) apply (fastforce elim: tcb_at_cte_at) apply (clarsimp simp: cte_at'_obj_at' tcb_cte_cases_def cte_map_def) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def) done crunch tcb'[wp]: setupReplyMaster "tcb_at' t" (wp: crunch_wps) crunch idle'[wp]: setupReplyMaster "valid_idle'" (* Levity: added (20090126 19:32:14) *) declare stateAssert_wp [wp] lemma setupReplyMaster_valid_mdb: "slot = t + 2 ^ objBits (undefined :: cte) * tcbReplySlot \ \valid_mdb' and valid_pspace' and tcb_at' t\ setupReplyMaster t \\rv. valid_mdb'\" apply (clarsimp simp: setupReplyMaster_def locateSlot_conv nullMDBNode_def) apply (fold initMDBNode_def) apply (wp setCTE_valid_mdb getCTE_wp') apply clarsimp apply (intro conjI) apply (case_tac cte) apply (fastforce simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def no_mdb_def elim: valid_nullcapsE) apply (frule obj_at_aligned') apply (simp add: valid_cap'_def capAligned_def objBits_def objBitsKO_def word_bits_def)+ apply (clarsimp simp: valid_pspace'_def) apply (clarsimp simp: caps_no_overlap'_def capRange_def) apply (clarsimp simp: fresh_virt_cap_class_def elim!: ranE) apply (clarsimp simp add: noReplyCapsFor_def cte_wp_at_ctes_of) apply (case_tac x) apply (rename_tac capability mdbnode) apply (case_tac capability; simp) apply (rename_tac arch_capability) apply (case_tac arch_capability; simp) apply fastforce done lemma setupReplyMaster_valid_objs [wp]: "\ valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t\ setupReplyMaster t \\_. valid_objs'\" apply (simp add: setupReplyMaster_def locateSlot_conv) apply (wp setCTE_valid_objs getCTE_wp') apply (clarsimp) apply (frule obj_at_aligned') apply (simp add: valid_cap'_def capAligned_def objBits_def objBitsKO_def word_bits_def)+ done lemma setupReplyMaster_wps[wp]: "\pspace_aligned'\ setupReplyMaster t \\rv. pspace_aligned'\" "\pspace_distinct'\ setupReplyMaster t \\rv. pspace_distinct'\" "slot = cte_map (t, tcb_cnode_index 2) \ \\s. P ((cteCaps_of s)(slot \ (capability.ReplyCap t True))) \ P (cteCaps_of s)\ setupReplyMaster t \\rv s. P (cteCaps_of s)\" apply (simp_all add: setupReplyMaster_def locateSlot_conv) apply (wp hoare_drop_imps | simp add: o_def | rule hoare_strengthen_post [OF getCTE_sp])+ apply (clarsimp elim!: rsubst[where P=P] intro!: ext) apply (clarsimp simp: tcbReplySlot_def objBits_def objBitsKO_def tcb_cnode_index_def2 cte_map_nat_to_cref cte_level_bits_def) done crunch no_0_obj'[wp]: setupReplyMaster no_0_obj' (wp: crunch_wps) lemma setupReplyMaster_valid_pspace': "\valid_pspace' and tcb_at' t\ setupReplyMaster t \\rv. valid_pspace'\" apply (simp add: valid_pspace'_def) apply (wp setupReplyMaster_valid_mdb) apply (simp_all add: valid_pspace'_def) done lemma setupReplyMaster_ifunsafe'[wp]: "slot = t + 2 ^ objBits (undefined :: cte) * tcbReplySlot \ \if_unsafe_then_cap' and ex_cte_cap_to' slot\ setupReplyMaster t \\rv s. if_unsafe_then_cap' s\" apply (simp add: ifunsafe'_def3 setupReplyMaster_def locateSlot_conv) apply (wp getCTE_wp') apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of cteCaps_of_def cte_level_bits_def objBits_simps) apply (drule_tac x=crefa in spec) apply (rule conjI) apply clarsimp apply (rule_tac x=cref in exI, fastforce) apply clarsimp apply (rule_tac x=cref' in exI, fastforce) done lemma setupReplyMaster_iflive'[wp]: "\if_live_then_nonz_cap'\ setupReplyMaster t \\rv. if_live_then_nonz_cap'\" apply (simp add: setupReplyMaster_def locateSlot_conv) apply (wp setCTE_iflive' getCTE_wp') apply (clarsimp elim!: cte_wp_at_weakenE') done lemma setupReplyMaster_global_refs[wp]: "\\s. valid_global_refs' s \ thread \ global_refs' s \ tcb_at' thread s \ ex_nonz_cap_to' thread s \ valid_objs' s\ setupReplyMaster thread \\rv. valid_global_refs'\" apply (simp add: setupReplyMaster_def locateSlot_conv) apply (wp getCTE_wp') apply (clarsimp simp: capRange_def cte_wp_at_ctes_of objBits_simps) apply (clarsimp simp: ex_nonz_cap_to'_def cte_wp_at_ctes_of) apply (rename_tac "prev_cte") apply (case_tac prev_cte, simp) apply (frule(1) ctes_of_valid_cap') apply (drule(1) valid_global_refsD_with_objSize)+ apply (clarsimp simp: valid_cap'_def objBits_simps obj_at'_def projectKOs split: capability.split_asm) done crunch valid_arch'[wp]: setupReplyMaster "valid_arch_state'" lemma ex_nonz_tcb_cte_caps': "\ex_nonz_cap_to' t s; tcb_at' t s; valid_objs' s; sl \ dom tcb_cte_cases\ \ ex_cte_cap_to' (t + sl) s" apply (clarsimp simp: ex_nonz_cap_to'_def ex_cte_cap_to'_def cte_wp_at_ctes_of) apply (subgoal_tac "s \' cteCap cte") apply (rule_tac x=cref in exI, rule_tac x=cte in exI) apply (clarsimp simp: valid_cap'_def obj_at'_def projectKOs dom_def split: cte.split_asm capability.split_asm) apply (case_tac cte) apply (clarsimp simp: ctes_of_valid_cap') done lemma ex_nonz_cap_not_global': "\ex_nonz_cap_to' t s; valid_objs' s; valid_global_refs' s\ \ t \ global_refs' s" apply (clarsimp simp: ex_nonz_cap_to'_def cte_wp_at_ctes_of) apply (frule(1) valid_global_refsD') apply clarsimp apply (drule orthD1, erule (1) subsetD) apply (subgoal_tac "s \' cteCap cte") apply (fastforce simp: valid_cap'_def capRange_def capAligned_def is_aligned_no_overflow split: cte.split_asm capability.split_asm) apply (case_tac cte) apply (clarsimp simp: ctes_of_valid_cap') done crunch typ_at'[wp]: setupReplyMaster "\s. P (typ_at' T p s)" (wp: hoare_drop_imps) lemma setCTE_irq_handlers': "\\s. valid_irq_handlers' s \ (\irq. cteCap cte = IRQHandlerCap irq \ irq_issued' irq s)\ setCTE ptr cte \\rv. valid_irq_handlers'\" apply (simp add: valid_irq_handlers'_def cteCaps_of_def irq_issued'_def) apply (wp hoare_use_eq [where f=ksInterruptState, OF setCTE_ksInterruptState setCTE_ctes_of_wp]) apply (auto simp: ran_def) done lemma setupReplyMaster_irq_handlers'[wp]: "\valid_irq_handlers'\ setupReplyMaster t \\rv. valid_irq_handlers'\" apply (simp add: setupReplyMaster_def locateSlot_conv) apply (wp setCTE_irq_handlers' getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of) done crunch irq_states' [wp]: setupReplyMaster valid_irq_states' crunch irqs_makes' [wp]: setupReplyMaster irqs_masked' (lift: irqs_masked_lift) crunch pde_mappings' [wp]: setupReplyMaster valid_pde_mappings' crunch pred_tcb_at' [wp]: setupReplyMaster "pred_tcb_at' proj P t" crunch ksMachine[wp]: setupReplyMaster "\s. P (ksMachineState s)" lemma setupReplyMaster_vms'[wp]: "\valid_machine_state'\ setupReplyMaster t \\_. valid_machine_state'\" apply (simp add: valid_machine_state'_def pointerInUserData_def ) apply (intro hoare_vcg_all_lift hoare_vcg_disj_lift) apply wp done crunch pspace_domain_valid[wp]: setupReplyMaster "pspace_domain_valid" crunch ct_not_inQ[wp]: setupReplyMaster "ct_not_inQ" crunch ksCurDomain[wp]: setupReplyMaster "\s. P (ksCurDomain s)" crunch ksCurThread[wp]: setupReplyMaster "\s. P (ksCurThread s)" crunch ksIdlethread[wp]: setupReplyMaster "\s. P (ksIdleThread s)" crunch ksDomSchedule[wp]: setupReplyMaster "\s. P (ksDomSchedule s)" crunch scheduler_action[wp]: setupReplyMaster "\s. P (ksSchedulerAction s)" crunch obj_at'_inQ[wp]: setupReplyMaster "obj_at' (inQ d p) t" crunch tcbDomain_inv[wp]: setupReplyMaster "obj_at' (\tcb. P (tcbDomain tcb)) t" crunch tcbPriority_inv[wp]: setupReplyMaster "obj_at' (\tcb. P (tcbPriority tcb)) t" crunch ready_queues[wp]: setupReplyMaster "\s. P (ksReadyQueues s)" crunch ready_queuesL1[wp]: setupReplyMaster "\s. P (ksReadyQueuesL1Bitmap s)" crunch ready_queuesL2[wp]: setupReplyMaster "\s. P (ksReadyQueuesL2Bitmap s)" crunch ksDomScheduleIdx[wp]: setupReplyMaster "\s. P (ksDomScheduleIdx s)" lemma setupReplyMaster_invs'[wp]: "\invs' and tcb_at' t and ex_nonz_cap_to' t\ setupReplyMaster t \\rv. invs'\" apply (simp add: invs'_def valid_state'_def) apply (rule hoare_pre) apply (wp setupReplyMaster_valid_pspace' sch_act_wf_lift tcb_in_cur_domain'_lift ct_idle_or_in_cur_domain'_lift valid_queues_lift cur_tcb_lift valid_queues_lift' hoare_vcg_disj_lift valid_irq_node_lift | simp)+ apply (clarsimp simp: ex_nonz_tcb_cte_caps' valid_pspace'_def objBits_def objBitsKO_def tcbReplySlot_def ex_nonz_cap_not_global' dom_def) done lemma setupReplyMaster_cte_wp_at'': "\cte_wp_at' (\cte. P (cteCap cte)) p and K (\ P NullCap)\ setupReplyMaster t \\rv s. cte_wp_at' (P \ cteCap) p s\" apply (simp add: setupReplyMaster_def locateSlot_conv tree_cte_cteCap_eq) apply (wp getCTE_wp') apply (fastforce simp: cte_wp_at_ctes_of cteCaps_of_def) done lemmas setupReplyMaster_cte_wp_at' = setupReplyMaster_cte_wp_at''[unfolded o_def] lemma setupReplyMaster_cap_to'[wp]: "\ex_nonz_cap_to' p\ setupReplyMaster t \\rv. ex_nonz_cap_to' p\" apply (simp add: ex_nonz_cap_to'_def) apply (rule hoare_pre) apply (wp hoare_vcg_ex_lift setupReplyMaster_cte_wp_at') apply clarsimp done definition is_arch_update' :: "capability \ cte \ bool" where "is_arch_update' cap cte \ isArchObjectCap cap \ capMasterCap cap = capMasterCap (cteCap cte)" lemma mdb_next_pres: "\ m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v) \ \ m(p \ x) \ a \ b = m \ a \ b" by (simp add: mdb_next_unfold) lemma mdb_next_trans_next_pres: "\ m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v) \ \ m(p \ x) \ a \\<^sup>+ b = m \ a \\<^sup>+ b" apply (rule iffI) apply (erule trancl_induct) apply (fastforce simp: mdb_next_pres) apply (erule trancl_trans) apply (rule r_into_trancl) apply (fastforce simp: mdb_next_pres) apply (erule trancl_induct) apply (rule r_into_trancl) apply (simp add: mdb_next_pres del: fun_upd_apply) apply (erule trancl_trans) apply (fastforce simp: mdb_next_pres simp del: fun_upd_apply) done lemma mdb_next_rtrans_next_pres: "\ m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v) \ \ m(p \ x) \ a \\<^sup>* b = m \ a \\<^sup>* b" by (simp add: rtrancl_eq_or_trancl mdb_next_trans_next_pres) lemma arch_update_descendants': "\ is_arch_update' cap oldcte; m p = Some oldcte\ \ descendants_of' x (m(p \ cteCap_update (\_. cap) oldcte)) = descendants_of' x m" apply (erule same_master_descendants) apply (auto simp: is_arch_update'_def isCap_simps) done lemma arch_update_setCTE_mdb: "\cte_wp_at' (is_arch_update' cap) p and cte_wp_at' (op = oldcte) p and valid_mdb'\ setCTE p (cteCap_update (\_. cap) oldcte) \\rv. valid_mdb'\" apply (simp add: valid_mdb'_def) apply wp apply (clarsimp simp: valid_mdb_ctes_def cte_wp_at_ctes_of simp del: fun_upd_apply) apply (rule conjI) apply (rule valid_dlistI) apply (fastforce split: split_if_asm elim: valid_dlistE) apply (fastforce split: split_if_asm elim: valid_dlistE) apply (rule conjI) apply (clarsimp simp: no_0_def) apply (rule conjI) apply (simp add: mdb_chain_0_def mdb_next_trans_next_pres) apply blast apply (rule conjI) apply (cases oldcte) apply (clarsimp simp: valid_badges_def mdb_next_pres simp del: fun_upd_apply) apply (clarsimp simp: is_arch_update'_def) apply (clarsimp split: split_if_asm) apply (clarsimp simp: isCap_simps) prefer 2 subgoal by fastforce apply (erule_tac x=pa in allE) apply (erule_tac x=p in allE) apply simp apply (simp add: sameRegionAs_def3) apply (rule conjI) apply (clarsimp simp: isCap_simps) apply (clarsimp simp: isCap_simps) apply (rule conjI) apply (clarsimp simp: caps_contained'_def simp del: fun_upd_apply) apply (cases oldcte) apply (clarsimp simp: is_arch_update'_def) apply (frule capMaster_untypedRange) apply (frule capMaster_capRange) apply (drule sym [where s="capMasterCap cap"]) apply (frule masterCap.intro) apply (clarsimp simp: masterCap.isUntypedCap split: split_if_asm) subgoal by fastforce subgoal by fastforce apply (erule_tac x=pa in allE) apply (erule_tac x=p in allE) apply fastforce apply (erule_tac x=pa in allE) apply (erule_tac x=p' in allE) subgoal by fastforce apply (rule conjI) apply (cases oldcte) apply (clarsimp simp: is_arch_update'_def) apply (clarsimp simp: mdb_chunked_def mdb_next_trans_next_pres simp del: fun_upd_apply) apply (drule sym [where s="capMasterCap cap"]) apply (frule masterCap.intro) apply (clarsimp split: split_if_asm) apply (erule_tac x=p in allE) apply (erule_tac x=p' in allE) apply (clarsimp simp: masterCap.sameRegionAs) apply (simp add: masterCap.sameRegionAs is_chunk_def mdb_next_trans_next_pres mdb_next_rtrans_next_pres) subgoal by fastforce apply (erule_tac x=pa in allE) apply (erule_tac x=p in allE) apply (clarsimp simp: masterCap.sameRegionAs) apply (simp add: masterCap.sameRegionAs is_chunk_def mdb_next_trans_next_pres mdb_next_rtrans_next_pres) subgoal by fastforce apply (erule_tac x=pa in allE) apply (erule_tac x=p' in allE) apply clarsimp apply (simp add: masterCap.sameRegionAs is_chunk_def mdb_next_trans_next_pres mdb_next_rtrans_next_pres) subgoal by fastforce apply (rule conjI) apply (clarsimp simp: is_arch_update'_def untyped_mdb'_def arch_update_descendants' simp del: fun_upd_apply) apply (cases oldcte) apply clarsimp apply (clarsimp split: split_if_asm) apply (clarsimp simp: isCap_simps) apply (frule capMaster_isUntyped) apply (drule capMaster_capRange) apply simp apply (rule conjI) apply (clarsimp simp: untyped_inc'_def arch_update_descendants' simp del: fun_upd_apply) apply (cases oldcte) apply (clarsimp simp: is_arch_update'_def) apply (drule capMaster_untypedRange) apply (clarsimp split: split_if_asm) apply (clarsimp simp: isCap_simps) apply (clarsimp simp: isCap_simps) apply (erule_tac x=pa in allE) apply (erule_tac x=p' in allE) apply clarsimp apply (rule conjI) apply (cases oldcte) apply (clarsimp simp: valid_nullcaps_def is_arch_update'_def isCap_simps) apply (rule conjI) apply (cases oldcte) apply (clarsimp simp: ut_revocable'_def is_arch_update'_def isCap_simps) apply (rule conjI) apply (clarsimp simp: class_links_def simp del: fun_upd_apply) apply (cases oldcte) apply (clarsimp simp: is_arch_update'_def mdb_next_pres) apply (drule capMaster_capClass) apply (clarsimp split: split_if_asm) apply fastforce apply (rule conjI) apply (erule(1) distinct_zombies_sameMasterE) apply (clarsimp simp: is_arch_update'_def) apply (clarsimp simp: irq_control_def) apply (cases oldcte) apply (subgoal_tac "cap \ IRQControlCap") prefer 2 apply (clarsimp simp: is_arch_update'_def isCap_simps) apply (rule conjI) apply clarsimp apply (simp add: reply_masters_rvk_fb_def) apply (erule ball_ran_fun_updI) apply (clarsimp simp add: is_arch_update'_def isCap_simps) done lemma capMaster_zobj_refs: "capMasterCap c = capMasterCap c' \ zobj_refs' c = zobj_refs' c'" by (simp add: capMasterCap_def split: capability.splits arch_capability.splits) lemma cte_refs_Master: "cte_refs' (capMasterCap cap) = cte_refs' cap" by (rule ext, simp add: capMasterCap_def split: capability.split) lemma zobj_refs_Master: "zobj_refs' (capMasterCap cap) = zobj_refs' cap" by (simp add: capMasterCap_def split: capability.split) lemma capMaster_same_refs: "capMasterCap a = capMasterCap b \ cte_refs' a = cte_refs' b \ zobj_refs' a = zobj_refs' b" apply (rule conjI) apply (rule master_eqI, rule cte_refs_Master, simp) apply (rule master_eqI, rule zobj_refs_Master, simp) done lemma arch_update_setCTE_iflive: "\cte_wp_at' (is_arch_update' cap) p and cte_wp_at' (op = oldcte) p and if_live_then_nonz_cap'\ setCTE p (cteCap_update (\_. cap) oldcte) \\rv. if_live_then_nonz_cap'\" apply (wp setCTE_iflive') apply (clarsimp simp: cte_wp_at_ctes_of is_arch_update'_def dest!: capMaster_zobj_refs) done lemma arch_update_setCTE_ifunsafe: "\cte_wp_at' (is_arch_update' cap) p and cte_wp_at' (op = oldcte) p and if_unsafe_then_cap'\ setCTE p (cteCap_update (\_. cap) oldcte) \\rv s. if_unsafe_then_cap' s\" apply (clarsimp simp: ifunsafe'_def2 cte_wp_at_ctes_of pred_conj_def) apply (rule hoare_lift_Pf2 [where f=irq_node']) prefer 2 apply wp apply (clarsimp simp: cte_wp_at_ctes_of is_arch_update'_def) apply (frule capMaster_same_refs) apply clarsimp apply (rule conjI, clarsimp) apply (erule_tac x=p in allE) apply clarsimp apply (erule impE) apply clarsimp apply clarsimp apply (rule_tac x=cref' in exI) apply clarsimp apply clarsimp apply (erule_tac x=cref in allE) apply clarsimp apply (rule_tac x=cref' in exI) apply clarsimp done lemma setCTE_cur_tcb[wp]: "\cur_tcb'\ setCTE ptr val \\rv. cur_tcb'\" by (wp cur_tcb_lift) lemma setCTE_vms'[wp]: "\valid_machine_state'\ setCTE ptr val \\rv. valid_machine_state'\" apply (simp add: valid_machine_state'_def pointerInUserData_def ) apply (intro hoare_vcg_all_lift hoare_vcg_disj_lift) apply wp done lemma arch_update_setCTE_invs: "\cte_wp_at' (is_arch_update' cap) p and cte_wp_at' (op = oldcte) p and invs' and valid_cap' cap\ setCTE p (cteCap_update (\_. cap) oldcte) \\rv. invs'\" apply (simp add: invs'_def valid_state'_def valid_pspace'_def) apply (rule hoare_pre) apply (wp arch_update_setCTE_mdb valid_queues_lift sch_act_wf_lift tcb_in_cur_domain'_lift ct_idle_or_in_cur_domain'_lift arch_update_setCTE_iflive arch_update_setCTE_ifunsafe valid_irq_node_lift setCTE_typ_at' setCTE_irq_handlers' valid_queues_lift' setCTE_pred_tcb_at' irqs_masked_lift setCTE_norq hoare_vcg_disj_lift | simp add: pred_tcb_at'_def)+ apply (clarsimp simp: valid_global_refs'_def is_arch_update'_def cte_wp_at_ctes_of isCap_simps) apply (frule capMaster_eq_capBits_eq) apply (drule capMaster_capRange) apply (clarsimp simp: valid_refs'_def valid_cap_sizes'_def) apply fastforce done definition "safe_parent_for' m p cap \ \parent node. m p = Some (CTE parent node) \ sameRegionAs parent cap \ ((\irq. cap = IRQHandlerCap irq) \ parent = IRQControlCap \ (\p n'. m p \ Some (CTE cap n')) \ isUntypedCap parent \ descendants_of' p m = {} \ capRange cap \ {} \ capBits cap \ capBits parent)" definition "is_simple_cap' cap \ cap \ NullCap \ cap \ IRQControlCap \ \ isUntypedCap cap \ \ isReplyCap cap \ \ isEndpointCap cap \ \ isNotificationCap cap \ \ isThreadCap cap \ \ isCNodeCap cap \ \ isZombie cap \ \ isArchPageCap cap" (* FIXME: duplicated *) locale mdb_insert_simple = mdb_insert + assumes safe_parent: "safe_parent_for' m src c'" assumes simple: "is_simple_cap' c'" begin lemma dest_no_parent_n: "n \ dest \ p = False" using src simple safe_parent apply clarsimp apply (erule subtree.induct) prefer 2 apply simp apply (clarsimp simp: parentOf_def mdb_next_unfold n_dest new_dest_def n) apply (cases "mdbNext src_node = dest") apply (subgoal_tac "m \ src \ dest") apply simp apply (subst mdb_next_unfold) apply (simp add: src) apply (clarsimp simp: isMDBParentOf_CTE) apply (clarsimp simp: is_simple_cap'_def revokable'_def) apply (cases c', auto simp: isCap_simps) apply (clarsimp simp add: sameRegionAs_def2) apply (clarsimp simp: isCap_simps) apply (clarsimp simp: safe_parent_for'_def isCap_simps) done lemma src_node_revokable [simp]: "mdbRevocable src_node" using safe_parent ut_rev src apply (clarsimp simp add: safe_parent_for'_def) apply (erule disjE) apply clarsimp apply (erule irq_revocable, rule irq_control) apply (clarsimp simp: ut_revocable'_def) done lemma new_child [simp]: "isMDBParentOf new_src new_dest" using safe_parent ut_rev src apply (simp add: new_src_def new_dest_def isMDBParentOf_def) apply (clarsimp simp: safe_parent_for'_def) apply (auto simp: isCap_simps) done lemma n_dest_child: "n \ src \ dest" apply (rule subtree.direct_parent) apply (simp add: n_direct_eq) apply simp apply (clarsimp simp: parentOf_def src dest n) done lemma parent_m_n: assumes "m \ p \ p'" shows "if p' = src then n \ p \ dest \ n \ p \ p' else n \ p \ p'" using assms proof induct case (direct_parent c) thus ?case apply (cases "p = src") apply simp apply (rule conjI, clarsimp) apply clarsimp apply (rule subtree.trans_parent [where c'=dest]) apply (rule n_dest_child) apply (simp add: n_direct_eq) apply simp apply (clarsimp simp: parentOf_def n) apply (clarsimp simp: new_src_def src) apply simp apply (subgoal_tac "n \ p \ c") prefer 2 apply (rule subtree.direct_parent) apply (clarsimp simp add: n_direct_eq) apply simp apply (clarsimp simp: parentOf_def n) apply (fastforce simp: new_src_def src) apply clarsimp apply (erule subtree_trans) apply (rule n_dest_child) done next case (trans_parent c d) thus ?case apply - apply (cases "c = dest", simp) apply (cases "d = dest", simp) apply (cases "c = src") apply clarsimp apply (erule subtree.trans_parent [where c'=dest]) apply (clarsimp simp add: n_direct_eq) apply simp apply (clarsimp simp: parentOf_def n) apply (rule conjI, clarsimp) apply (clarsimp simp: new_src_def src) apply clarsimp apply (subgoal_tac "n \ p \ d") apply clarsimp apply (erule subtree_trans, rule n_dest_child) apply (erule subtree.trans_parent) apply (simp add: n_direct_eq) apply simp apply (clarsimp simp: parentOf_def n) apply (fastforce simp: src new_src_def) done qed lemma n_to_dest [simp]: "n \ p \ dest = (p = src)" by (simp add: n_direct_eq) lemma parent_n_m: assumes "n \ p \ p'" shows "if p' = dest then p \ src \ m \ p \ src else m \ p \ p'" proof - from assms have [simp]: "p \ dest" by (clarsimp simp: dest_no_parent_n) from assms show ?thesis proof induct case (direct_parent c) thus ?case apply simp apply (rule conjI) apply clarsimp apply clarsimp apply (rule subtree.direct_parent) apply (simp add: n_direct_eq split: split_if_asm) apply simp apply (clarsimp simp: parentOf_def n src new_src_def split: split_if_asm) done next case (trans_parent c d) thus ?case apply clarsimp apply (rule conjI, clarsimp) apply (clarsimp split: split_if_asm) apply (simp add: n_direct_eq) apply (cases "p=src") apply simp apply (rule subtree.direct_parent, assumption, assumption) apply (clarsimp simp: parentOf_def n src new_src_def split: split_if_asm) apply clarsimp apply (erule subtree.trans_parent, assumption, assumption) apply (clarsimp simp: parentOf_def n src new_src_def split: split_if_asm) apply (erule subtree.trans_parent) apply (simp add: n_direct_eq split: split_if_asm) apply assumption apply (clarsimp simp: parentOf_def n src new_src_def split: split_if_asm) done qed qed lemma descendants: "descendants_of' p n = (if src \ descendants_of' p m \ p = src then descendants_of' p m \ {dest} else descendants_of' p m)" apply (rule set_eqI) apply (simp add: descendants_of'_def) apply (fastforce dest!: parent_n_m dest: parent_m_n simp: n_dest_child split: split_if_asm) done end declare split_if [split del] lemma safe_parent_for_maskedAsFull[simp]: "safe_parent_for' m p (maskedAsFull src_cap a) = safe_parent_for' m p src_cap" apply (clarsimp simp:safe_parent_for'_def) apply (rule iffI) apply (clarsimp simp:maskedAsFull_def isCap_simps split:if_splits cap.splits cong:sameRegionAs_update_untyped')+ done lemma setUntypedCapAsFull_safe_parent_for': "\\s. safe_parent_for' (ctes_of s) slot a \ cte_wp_at' (op = srcCTE) slot s\ setUntypedCapAsFull (cteCap srcCTE) c' slot \\rv s. safe_parent_for' (ctes_of s) slot a\" apply (clarsimp simp:safe_parent_for'_def setUntypedCapAsFull_def split:if_splits) apply (intro conjI impI) apply (wp updateCap_ctes_of_wp) apply (subgoal_tac "mdb_inv_preserve (ctes_of s) (modify_map (ctes_of s) slot (cteCap_update (\_. capFreeIndex_update (\_. max_free_index (capBlockSize c')) (cteCap srcCTE))))") apply (frule mdb_inv_preserve.descendants_of[where p = slot]) apply (clarsimp simp:isCap_simps modify_map_def cte_wp_at_ctes_of simp del:fun_upd_apply) apply (clarsimp cong:sameRegionAs_update_untyped) apply (rule mdb_inv_preserve_updateCap) apply (simp add:cte_wp_at_ctes_of) apply simp apply wp apply simp done lemma maskedAsFull_revokable_safe_parent: "\is_simple_cap' c'; safe_parent_for' m p c'; m p = Some cte; cteCap cte = (maskedAsFull src_cap' a)\ \ revokable' (maskedAsFull src_cap' a) c' = revokable' src_cap' c'" apply (clarsimp simp:revokable'_def maskedAsFull_def split:if_splits) apply (intro allI impI conjI) apply (clarsimp simp:isCap_simps is_simple_cap'_def)+ done lemma is_simple_cap'_maskedAsFull[simp]: "is_simple_cap' (maskedAsFull src_cap' c') = is_simple_cap' src_cap'" by (auto simp: is_simple_cap'_def maskedAsFull_def isCap_simps split:if_splits) lemma cins_corres_simple: assumes "cap_relation c c'" "src' = cte_map src" "dest' = cte_map dest" notes trans_state_update'[symmetric,simp] shows "corres dc (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=cap.NullCap) dest and K (is_simple_cap c) and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s)) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and K (is_simple_cap' c') and cte_wp_at' (\c. cteCap c=NullCap) dest' and (\s. safe_parent_for' (ctes_of s) src' c')) (cap_insert c src dest) (cteInsert c' src' dest')" (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _ and _) _ _") using assms unfolding cap_insert_def cteInsert_def apply (fold revokable_def revokable'_fold) apply simp apply (rule corres_guard_imp) apply (rule corres_split [OF _ get_cap_corres]) apply (rule corres_split [OF _ get_cap_corres]) apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at (op = src_cap) src" and Q="?P' and cte_wp_at' (op = rv') (cte_map dest) and cte_wp_at' (op = srcCTE) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) apply (case_tac rv') apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) apply (simp add: nullPointer_def) apply (rule corres_guard_imp) apply (rule_tac R="\r. ?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at (op = (masked_as_full src_cap c)) src" and R'="\r. ?P' and cte_wp_at' (op = rv') (cte_map dest) and cte_wp_at' (op = (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_split[where r'=dc]) apply (rule corres_stronger_no_failI) apply (rule no_fail_pre, wp hoare_weak_lift_imp) apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def) apply (erule_tac valid_dlistEn[where p = "cte_map src"]) apply (simp+)[3] apply (clarsimp simp: corres_underlying_def state_relation_def in_monad valid_mdb'_def valid_mdb_ctes_def) apply (drule (1) pspace_relationsD) apply (drule (18) set_cap_not_quite_corres) apply (rule refl) apply (elim conjE exE) apply (rule bind_execI, assumption) apply (subgoal_tac "mdb_insert_abs (cdt a) src dest") prefer 2 apply (clarsimp simp: cte_wp_at_caps_of_state valid_mdb_def2) apply (rule mdb_insert_abs.intro) apply clarsimp apply (erule (1) mdb_cte_at_Null_None) apply (erule (1) mdb_cte_at_Null_descendants) apply (subgoal_tac "no_mloop (cdt a)") prefer 2 apply (simp add: valid_mdb_def) apply (clarsimp simp: exec_gets update_cdt_def bind_assoc set_cdt_def exec_get exec_put set_original_def modify_def simp del: fun_upd_apply | (rule bind_execI[where f="cap_insert_ext x y z x' y'" for x y z x' y'], clarsimp simp: mdb_insert_abs.cap_insert_ext_det_def2 update_cdt_list_def set_cdt_list_def put_def simp del: fun_upd_apply) | rule refl)+ apply (clarsimp simp: put_def state_relation_def simp del: fun_upd_apply) apply (drule updateCap_stuff) apply clarsimp apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) apply (clarsimp simp: pspace_relations_def) apply (rule conjI) apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv) apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def prev_update_modify_mdb_relation) apply (subgoal_tac "cte_map dest \ 0") prefer 2 apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def) apply (subgoal_tac "cte_map src \ 0") prefer 2 apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def) apply (thin_tac "ksMachineState t = p" for t p)+ apply (thin_tac "ksCurThread t = p" for t p)+ apply (thin_tac "ksIdleThread t = p" for t p)+ apply (thin_tac "ksReadyQueues t = p" for t p)+ apply (thin_tac "ksSchedulerAction t = p" for t p)+ apply (subgoal_tac "should_be_parent_of src_cap (is_original_cap a src) c (revokable src_cap c) = True") prefer 2 apply (subst should_be_parent_of_masked_as_full[symmetric]) apply (subst safe_parent_is_parent) apply (simp add: cte_wp_at_caps_of_state) apply (simp add: cte_wp_at_caps_of_state) apply simp apply simp apply (subst conj_assoc[symmetric]) apply (rule conjI) defer apply (thin_tac "ctes_of t = t'" for t t')+ apply (clarsimp simp: modify_map_apply) apply (clarsimp simp: revokable_relation_def simp del: fun_upd_apply) apply (simp split: split_if) apply (rule conjI) apply clarsimp apply (subgoal_tac "mdbRevocable node = revokable' (cteCap srcCTE) c'") prefer 2 apply (case_tac rv') apply (clarsimp simp add: const_def modify_map_def split: split_if_asm) apply clarsimp apply (rule revokable_eq, assumption, assumption) apply (subst same_region_as_relation [symmetric]) prefer 3 apply (rule safe_parent_same_region) apply (simp add: cte_wp_at_caps_of_state safe_parent_for_masked_as_full) apply assumption apply assumption apply (clarsimp simp: cte_wp_at_def is_simple_cap_def) apply clarsimp apply (case_tac srcCTE) apply (case_tac rv') apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 subgoal by (clarsimp simp: modify_map_def split: split_if_asm) apply clarsimp apply (drule set_cap_caps_of_state_monad)+ apply (subgoal_tac "null_filter (caps_of_state a) (aa,bb) \ None") prefer 2 subgoal by (clarsimp simp: cte_wp_at_caps_of_state null_filter_def split: if_splits) apply clarsimp apply (subgoal_tac "cte_at (aa,bb) a") prefer 2 apply (drule null_filter_caps_of_stateD) apply (erule cte_wp_at_weakenE, rule TrueI) apply (subgoal_tac "mdbRevocable node = mdbRevocable node'") apply clarsimp apply (subgoal_tac "cte_map (aa,bb) \ cte_map dest") subgoal by (clarsimp simp: modify_map_def split: split_if_asm) apply (erule (5) cte_map_inj) apply (rule set_untyped_cap_as_full_corres) apply simp+ apply (wp set_untyped_cap_full_valid_objs set_untyped_cap_as_full_valid_mdb set_untyped_cap_as_full_valid_list set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at setUntypedCapAsFull_safe_parent_for' | clarsimp | wps)+ apply (clarsimp simp:cte_wp_at_caps_of_state ) apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp) apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) subgoal by (clarsimp simp: cte_wp_at'_def) apply (thin_tac "ctes_of s = t" for s t)+ apply (thin_tac "pspace_relation s t" for s t)+ apply (thin_tac "machine_state t = s" for t s)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) apply (case_tac "rv'") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ safe_parent_for (cdt a) src c src_cap") prefer 2 subgoal by (fastforce simp: cte_wp_at_def safe_parent_for_masked_as_full) apply (erule conjE) apply (subgoal_tac "mdb_insert (ctes_of b) (cte_map src) (maskedAsFull src_cap' c') src_node (cte_map dest) NullCap dest_node") prefer 2 apply (rule mdb_insert.intro) apply (rule mdb_ptr.intro) apply (rule vmdb.intro, simp add: valid_mdb_ctes_def) apply (erule mdb_ptr_axioms.intro) apply (rule mdb_ptr.intro) apply (rule vmdb.intro, simp add: valid_mdb_ctes_def) apply (erule mdb_ptr_axioms.intro) apply (rule mdb_insert_axioms.intro) apply (rule refl) apply assumption apply assumption apply assumption apply assumption apply (erule (5) cte_map_inj) apply (rule conjI) apply (simp (no_asm_simp) add: cdt_relation_def split: split_if) apply (intro impI allI) apply (frule mdb_insert_simple_axioms.intro) apply(clarsimp simp:cte_wp_at_ctes_of) apply (drule (1) mdb_insert_simple.intro) apply (drule_tac src_cap' = src_cap' in maskedAsFull_revokable_safe_parent[symmetric]) apply simp+ apply (subst mdb_insert_simple.descendants) apply simp apply (subst mdb_insert_abs.descendants_child, assumption) apply (frule set_cap_caps_of_state_monad) apply (subgoal_tac "cte_at (aa,bb) a") prefer 2 apply (clarsimp simp: cte_wp_at_caps_of_state split: split_if_asm) apply (simp add: descendants_of_eq' cdt_relation_def split: split_if del: split_paired_All) apply clarsimp apply (drule (5) cte_map_inj)+ apply simp (* exact reproduction of proof in cins_corres, as it does not used is_derived *) apply(simp add: cdt_list_relation_def del: split_paired_All split_paired_Ex) apply(subgoal_tac "no_mloop (cdt a) \ finite_depth (cdt a)") prefer 2 apply(simp add: finite_depth valid_mdb_def) apply(intro impI allI) apply(simp add: fun_upd_twist) apply(subst next_slot_eq[OF mdb_insert_abs.next_slot]) apply(simp_all del: fun_upd_apply) apply(simp split: option.splits del: fun_upd_apply add: fun_upd_twist) apply(intro allI impI) apply(subgoal_tac "src \ (aa, bb)") prefer 2 apply(rule notI) apply(simp add: valid_mdb_def no_mloop_weaken) apply(subst fun_upd_twist, simp, simp) apply(case_tac "ca=src") apply(simp) apply(clarsimp simp: modify_map_def) subgoal by(fastforce split: split_if_asm) apply(case_tac "ca = dest") apply(simp) apply(case_tac "next_slot src (cdt_list (a)) (cdt a)") apply(simp) apply(simp) apply(clarsimp simp: modify_map_def const_def) apply(simp split: split_if_asm) apply(drule_tac p="cte_map src" in valid_mdbD1') apply(simp) apply(simp add: valid_mdb'_def valid_mdb_ctes_def) apply(clarsimp) apply(drule cte_map_inj_eq) apply(simp_all)[6] apply(erule_tac x="fst src" in allE) apply(erule_tac x="snd src" in allE) apply(fastforce) apply(simp) apply(case_tac "next_slot ca (cdt_list (a)) (cdt a)") apply(simp) apply(simp) apply(subgoal_tac "cte_at ca a") prefer 2 apply(rule cte_at_next_slot) apply(simp_all)[5] apply(clarsimp simp: modify_map_def const_def) apply(simp split: split_if_asm) apply(drule cte_map_inj_eq) apply(simp_all)[6] apply(drule_tac p="cte_map src" in valid_mdbD1') apply(simp) apply(simp add: valid_mdb'_def valid_mdb_ctes_def) apply(clarsimp) apply(clarsimp) apply(case_tac z) apply(erule_tac x=aa in allE) apply(erule_tac x=bb in allE) apply(fastforce) apply(drule cte_map_inj_eq) apply(simp_all)[6] apply(drule cte_map_inj_eq) apply(simp_all)[6] apply(drule cte_map_inj_eq) apply(simp_all)[6] by(fastforce) declare split_if [split] lemma sameRegion_capRange_sub: "sameRegionAs cap cap' \ capRange cap' \ capRange cap" apply (clarsimp simp: sameRegionAs_def2 isCap_Master capRange_Master) apply (erule disjE) apply (clarsimp dest!: capMaster_capRange) apply (erule disjE) apply fastforce apply (clarsimp simp: isCap_simps capRange_def) done lemma safe_parent_for_capRange_capBits: "\ safe_parent_for' m p cap; m p = Some cte \ \ capRange cap \ capRange (cteCap cte) \ capBits cap \ capBits (cteCap cte)" apply (clarsimp simp: safe_parent_for'_def) apply (erule disjE) apply (clarsimp simp: capRange_def) by (auto simp: sameRegionAs_def2 isCap_simps capRange_def capMasterCap_def capRange_Master objBits_simps split:capability.splits arch_capability.splits) lemma safe_parent_Null: "\ m src = Some (CTE NullCap n); safe_parent_for' m src c' \ \ False" by (simp add: safe_parent_for'_def) lemma notUntypedRange: "\isUntypedCap cap \ untypedRange cap = {}" by (cases cap) (auto simp: isCap_simps) lemma safe_parent_for_untypedRange: "\ safe_parent_for' m p cap; m p = Some cte \ \ untypedRange cap \ untypedRange (cteCap cte)" apply (clarsimp simp: safe_parent_for'_def) apply (erule disjE) apply clarsimp apply clarsimp apply (simp add: sameRegionAs_def2) apply (erule disjE) apply clarsimp apply (drule capMaster_untypedRange) apply blast apply (erule disjE) apply (clarsimp simp: capRange_Master untypedCapRange) apply (cases "isUntypedCap cap") apply (clarsimp simp: capRange_Master untypedCapRange) apply blast apply (drule notUntypedRange) apply simp apply (clarsimp simp: isCap_Master isCap_simps) done lemma safe_parent_for_capUntypedRange: "\ safe_parent_for' m p cap; m p = Some cte \ \ capRange cap \ untypedRange (cteCap cte)" apply (clarsimp simp: safe_parent_for'_def) apply (erule disjE) apply (clarsimp simp: capRange_def) apply clarsimp apply (simp add: sameRegionAs_def2) apply (erule disjE) apply clarsimp apply (frule capMaster_capRange) apply (clarsimp simp: capRange_Master untypedCapRange) apply (erule disjE) apply (clarsimp simp: capRange_Master untypedCapRange) apply blast apply (clarsimp simp: isCap_Master isCap_simps) done lemma safe_parent_for_descendants': "\ safe_parent_for' m p cap; m p = Some (CTE pcap n); isUntypedCap pcap \ \ descendants_of' p m = {}" by (auto simp: safe_parent_for'_def isCap_simps) lemma safe_parent_not_ep': "\ safe_parent_for' m p cap; m p = Some (CTE src_cap n) \ \ \isEndpointCap src_cap" by (auto simp: safe_parent_for'_def isCap_simps) lemma safe_parent_not_ntfn': "\ safe_parent_for' m p cap; m p = Some (CTE src_cap n) \ \ \isNotificationCap src_cap" by (auto simp: safe_parent_for'_def isCap_simps) lemma safe_parent_capClass: "\ safe_parent_for' m p cap; m p = Some (CTE src_cap n) \ \ capClass cap = capClass src_cap" by (auto simp: safe_parent_for'_def isCap_simps sameRegionAs_def2 capRange_Master capRange_def capMasterCap_def split: capability.splits arch_capability.splits) locale mdb_insert_simple' = mdb_insert_simple + fixes n' defines "n' \ modify_map n (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\_. dest)))" begin lemma no_0_n' [intro!]: "no_0 n'" by (auto simp: n'_def) lemmas n_0_simps' [iff] = no_0_simps [OF no_0_n'] lemmas no_0_m_prev [iff] = no_0_prev [OF no_0] lemmas no_0_n_prev [iff] = no_0_prev [OF no_0_n'] lemma chain_n': "mdb_chain_0 n'" unfolding n'_def by (rule mdb_chain_0_modify_map_prev) (rule chain_n) lemma no_loops_n': "no_loops n'" using chain_n' no_0_n' by (rule mdb_chain_0_no_loops) lemma irrefl_direct_simp_n' [iff]: "n' \ x \ x = False" using no_loops_n' by (rule no_loops_direct_simp) lemma irrefl_trancl_simp' [iff]: "n \ x \\<^sup>+ x = False" using no_loops_n by (rule no_loops_trancl_simp) lemma n_direct_eq': "n' \ p \ p' = (if p = src then p' = dest else if p = dest then m \ src \ p' else m \ p \ p')" by (simp add: n'_def mdb_next_modify n_direct_eq) lemma dest_no_next_p: "m p = Some cte \ mdbNext (cteMDBNode cte) \ dest" using dest dest_prev apply (cases cte) apply (rule notI) apply (rule dlistEn, assumption) apply clarsimp apply clarsimp done lemma dest_no_src_next [iff]: "mdbNext src_node \ dest" using src by (clarsimp dest!: dest_no_next_p) lemma n_dest': "n' dest = Some new_dest" by (simp add: n'_def n modify_map_if new_dest_def) lemma n_src_dest': "n' \ src \ dest" by (simp add: n_src_dest n'_def) lemma dest_chain_0' [simp, intro!]: "n' \ dest \\<^sup>+ 0" using chain_n' n_dest' by (simp add: mdb_chain_0_def) blast lemma n'_trancl_eq': "n' \ p \\<^sup>+ p' = (if p' = dest then m \ p \\<^sup>* src else if p = dest then m \ src \\<^sup>+ p' else m \ p \\<^sup>+ p')" unfolding n'_def trancl_prev_update by (simp add: n_trancl_eq') lemma n'_trancl_eq: "n' \ p \\<^sup>+ p' = (if p' = dest then p = src \ m \ p \\<^sup>+ src else if p = dest then m \ src \\<^sup>+ p' else m \ p \\<^sup>+ p')" unfolding n'_def trancl_prev_update by (simp add: n_trancl_eq) lemma n_rtrancl_eq': "n' \ p \\<^sup>* p' = (if p' = dest then p = dest \ p \ dest \ m \ p \\<^sup>* src else if p = dest then p' \ src \ m \ src \\<^sup>* p' else m \ p \\<^sup>* p')" unfolding n'_def rtrancl_prev_update by (simp add: n_rtrancl_eq) lemma n'_cap: "n' p = Some (CTE cap node) \ \node'. if p = dest then cap = c' \ m p = Some (CTE dest_cap node') else m p = Some (CTE cap node')" by (auto simp add: n'_def n src dest new_src_def new_dest_def modify_map_if split: split_if_asm) lemma n'_rev: "n' p = Some (CTE cap node) \ \node'. if p = dest then mdbRevocable node = revokable' src_cap c' \ m p = Some (CTE dest_cap node') else m p = Some (CTE cap node') \ mdbRevocable node = mdbRevocable node'" by (auto simp add: n'_def n src dest new_src_def new_dest_def modify_map_if split: split_if_asm) lemma m_cap': "m p = Some (CTE cap node) \ \node'. if p = dest then cap = dest_cap \ n' p = Some (CTE c' node') else n' p = Some (CTE cap node')" apply (simp add: n'_def n new_src_def new_dest_def modify_map_if) apply (cases "p=dest") apply (auto simp: src dest) done lemma dest_no_parent_n' [simp]: "n' \ dest \ p = False" by (simp add: n'_def dest_no_parent_n) lemma descendants': "descendants_of' p n' = (if src \ descendants_of' p m \ p = src then descendants_of' p m \ {dest} else descendants_of' p m)" by (simp add: n'_def descendants descendants_of_prev_update) lemma ut_revocable_n' [simp]: "ut_revocable' n'" using dest apply (clarsimp simp: ut_revocable'_def) apply (frule n'_cap) apply (drule n'_rev) apply clarsimp apply (clarsimp simp: n_dest' new_dest_def split: split_if_asm) apply (clarsimp simp: revokable'_def isCap_simps) apply (drule_tac p=p and m=m in ut_revocableD', assumption) apply (rule ut_rev) apply simp done lemma valid_nc' [simp]: "valid_nullcaps n'" unfolding valid_nullcaps_def using src dest dest_prev dest_next simple safe_parent apply (clarsimp simp: n'_def n_def modify_map_if) apply (rule conjI) apply (clarsimp simp: is_simple_cap'_def) apply clarsimp apply (rule conjI) apply (fastforce dest!: safe_parent_Null) apply clarsimp apply (rule conjI) apply clarsimp apply (drule (1) valid_nullcaps_next, rule no_0, rule dlist, rule nullcaps) apply simp apply clarsimp apply (erule nullcapsD', rule nullcaps) done lemma n'_prev_eq: "n' \ p \ p' = (if p' = mdbNext src_node \ p' \ 0 then p = dest else if p' = dest then p = src else m \ p \ p')" using src dest dest_prev dest_next apply (cases "p' = 0", simp) apply (simp split del: split_if) apply (cases "p' = mdbNext src_node") apply (clarsimp simp: modify_map_apply n'_def n_def mdb_prev_def) apply (clarsimp simp: modify_map_if) apply (rule iffI, clarsimp) apply clarsimp apply (rule dlistEn, assumption, simp) apply clarsimp apply (case_tac cte') apply clarsimp apply (cases "p' = dest") apply (clarsimp simp: modify_map_if n'_def n_def mdb_prev_def) apply clarsimp apply (clarsimp simp: modify_map_if n'_def n_def mdb_prev_def) apply (cases "p' = src", simp) apply clarsimp apply (rule iffI, clarsimp) apply clarsimp apply (case_tac z) apply clarsimp done lemma m_prev_of_next: "m \ p \ mdbNext src_node = (p = src \ mdbNext src_node \ 0)" using src apply (clarsimp simp: mdb_prev_def) apply (rule iffI) apply clarsimp apply (rule dlistEn, assumption, clarsimp) apply clarsimp apply clarsimp apply (rule dlistEn, assumption, clarsimp) apply clarsimp done lemma src_next_eq: "m \ p \ mdbNext src_node = (if mdbNext src_node \ 0 then p = src else m \ p \ 0)" using src apply - apply (rule iffI) prefer 2 apply (clarsimp split: split_if_asm) apply clarsimp apply (rule conjI) apply clarsimp apply (frule (1) dlist_nextD0) apply (clarsimp simp: m_prev_of_next) apply clarsimp done lemma src_next_eq': "m (mdbNext src_node) = Some cte \ m \ p \ mdbNext src_node = (p = src)" by (subst src_next_eq) auto lemma dest_no_prev [iff]: "\ m \ dest \ p" using dest dest_next apply (clarsimp simp: mdb_prev_def) apply (rule dlistEp [where p=p], assumption, clarsimp) apply clarsimp done lemma src_prev [iff]: "m \ src \ p = (p = mdbNext src_node \ p \ 0)" using src apply - apply (rule iffI) prefer 2 apply (clarsimp simp: mdb_ptr_src.next_p_prev) apply (clarsimp simp: mdb_prev_def) apply (rule conjI) prefer 2 apply clarsimp apply (rule dlistEp [where p=p], assumption, clarsimp) apply simp done lemma blurg: "(\c c'. Q c \ P c') = (\c. Q c \ (\c'. P c'))" apply simp done lemma dlist' [simp]: "valid_dlist n'" using src dest apply (unfold valid_dlist_def3 n_direct_eq' n'_prev_eq) apply (split split_if) apply (split split_if) apply (split split_if) apply (split split_if) apply (split split_if) apply (split split_if) apply (split split_if) apply simp apply (intro conjI impI allI notI) apply (fastforce simp: src_next_eq') apply (clarsimp simp: src_next_eq split: split_if_asm) apply (simp add: mdb_ptr_src.p_next) apply (erule (1) dlist_nextD0) apply clarsimp apply clarsimp apply clarsimp apply (erule (1) dlist_prevD0) done lemma utRange_c': "untypedRange c' \ untypedRange src_cap" using safe_parent src by - (drule (1) safe_parent_for_untypedRange, simp) lemma capRange_c': "capRange c' \ capRange src_cap" using safe_parent src by - (drule (1) safe_parent_for_capRange_capBits, simp) lemma not_ut_c' [simp]: "\isUntypedCap c'" using simple by (simp add: is_simple_cap'_def) lemma utCapRange_c': "capRange c' \ untypedRange src_cap" using safe_parent src by - (drule (1) safe_parent_for_capUntypedRange, simp) lemma ut_descendants: "isUntypedCap src_cap \ descendants_of' src m = {}" using safe_parent src by (rule safe_parent_for_descendants') lemma ut_mdb' [simp]: "untyped_mdb' n'" using src dest utRange_c' capRange_c' utCapRange_c' apply (clarsimp simp: untyped_mdb'_def) apply (drule n'_cap)+ apply (clarsimp simp: descendants') apply (clarsimp split: split_if_asm) apply (cases "isUntypedCap src_cap") prefer 2 apply (drule_tac p=p and p'=src and m=m in untyped_mdbD', assumption+) apply blast apply (rule untyped_mdb) apply simp apply (frule ut_descendants) apply (drule (3) untyped_incD', rule untyped_inc) apply clarsimp apply blast apply (fastforce elim: untyped_mdbD' intro!: untyped_mdb) done lemma n'_badge: "n' p = Some (CTE cap node) \ \node'. if p = dest then mdbFirstBadged node = revokable' src_cap c' \ m p = Some (CTE dest_cap node') else m p = Some (CTE cap node') \ mdbFirstBadged node = mdbFirstBadged node'" by (auto simp add: n'_def n src dest new_src_def new_dest_def modify_map_if split: split_if_asm) lemma src_not_ep [simp]: "\isEndpointCap src_cap" using safe_parent src by (rule safe_parent_not_ep') lemma src_not_ntfn [simp]: "\isNotificationCap src_cap" using safe_parent src by (rule safe_parent_not_ntfn') lemma c_not_ep [simp]: "\isEndpointCap c'" using simple by (simp add: is_simple_cap'_def) lemma c_not_ntfn [simp]: "\isNotificationCap c'" using simple by (simp add: is_simple_cap'_def) lemma valid_badges' [simp]: "valid_badges n'" using simple src dest apply (clarsimp simp: valid_badges_def) apply (simp add: n_direct_eq') apply (frule_tac p=p in n'_badge) apply (frule_tac p=p' in n'_badge) apply (drule n'_cap)+ apply (clarsimp split: split_if_asm) apply (insert valid_badges) apply (simp add: valid_badges_def) apply blast done lemma caps_contained' [simp]: "caps_contained' n'" using src dest capRange_c' utCapRange_c' apply (clarsimp simp: caps_contained'_def) apply (drule n'_cap)+ apply clarsimp apply (clarsimp split: split_if_asm) apply (drule capRange_untyped) apply simp apply (drule capRange_untyped) apply clarsimp apply (cases "isUntypedCap src_cap") prefer 2 apply (drule_tac p=p and p'=src in caps_containedD', assumption+) apply blast apply (rule caps_contained) apply blast apply (frule capRange_untyped) apply (drule (3) untyped_incD', rule untyped_inc) apply (clarsimp simp: ut_descendants) apply blast apply (drule (3) caps_containedD', rule caps_contained) apply blast done lemma capClass_c' [simp]: "capClass c' = capClass src_cap" using safe_parent src by (rule safe_parent_capClass) lemma class_links' [simp]: "class_links n'" using src dest apply (clarsimp simp: class_links_def) apply (simp add: n_direct_eq') apply (case_tac cte, case_tac cte') apply clarsimp apply (drule n'_cap)+ apply clarsimp apply (clarsimp split: split_if_asm) apply (drule (2) class_linksD, rule class_links) apply simp apply (drule (2) class_linksD, rule class_links) apply simp done lemma untyped_inc' [simp]: "untyped_inc' n'" using src dest apply (clarsimp simp: untyped_inc'_def) apply (drule n'_cap)+ apply (clarsimp simp: descendants') apply (clarsimp split: split_if_asm) apply (rule conjI) apply clarsimp apply (drule (3) untyped_incD', rule untyped_inc) apply clarsimp apply (rule conjI) apply clarsimp apply (frule_tac p=src and p'=p' in untyped_incD', assumption+, rule untyped_inc) apply (clarsimp simp: ut_descendants) apply (intro conjI, clarsimp+) apply (drule (3) untyped_incD', rule untyped_inc) apply clarsimp done lemma sameRegion_src [simp]: "sameRegionAs src_cap c'" using safe_parent src apply (simp add: safe_parent_for'_def) done lemma sameRegion_src_c': "sameRegionAs cap src_cap \ sameRegionAs cap c'" using safe_parent simple src capRange_c' apply (simp add: safe_parent_for'_def) apply (erule disjE) apply (clarsimp simp: sameRegionAs_def2 isCap_simps capRange_def) apply clarsimp apply (simp add: sameRegionAs_def2 isCap_Master capRange_Master) apply (erule disjE) prefer 2 apply (clarsimp simp: isCap_simps) apply (elim conjE) apply (erule disjE) prefer 2 apply (clarsimp simp: isCap_simps) apply simp apply blast done lemma sameRegion_c_src': "sameRegionAs c' cap \ sameRegionAs src_cap cap" using safe_parent simple src capRange_c' apply (simp add: safe_parent_for'_def) apply (erule disjE) apply clarsimp apply (clarsimp simp: sameRegionAs_def2 capRange_def isCap_simps) apply clarsimp apply (simp add: sameRegionAs_def2 isCap_Master capRange_Master) apply (erule disjE) prefer 2 apply clarsimp apply (erule disjE, blast) apply (clarsimp simp: isCap_simps) apply (clarsimp simp: capRange_def) apply (elim conjE) apply (drule capMaster_capRange) apply simp done lemma safe_not_next_region: "\ m \ src \ p; m p = Some (CTE cap node) \ \ \ sameRegionAs c' cap" using safe_parent src unfolding safe_parent_for'_def apply clarsimp apply (erule disjE) apply (clarsimp simp: mdb_next_unfold) apply (clarsimp simp: sameRegionAs_def2 isCap_simps) apply (clarsimp simp: descendants_of'_def) apply (erule_tac x=p in allE) apply (erule notE, rule direct_parent, assumption) apply clarsimp apply (simp add: parentOf_def) apply (simp add: isMDBParentOf_def) apply (erule sameRegionAs_trans [rotated]) apply (rule sameRegion_src) done lemma irq_c'_new: assumes irq_src: "isIRQControlCap src_cap" shows "m p = Some (CTE cap node) \ \ sameRegionAs c' cap" using safe_parent irq_src src apply (clarsimp simp: safe_parent_for'_def isCap_simps) apply (clarsimp simp: sameRegionAs_def2 isCap_simps) done lemma ut_capRange_non_empty: "isUntypedCap src_cap \ capRange c' \ {}" using safe_parent src unfolding safe_parent_for'_def by (clarsimp simp: isCap_simps) lemma ut_sameRegion_non_empty: "\ isUntypedCap src_cap; sameRegionAs c' cap \ \ capRange cap \ {}" using simple safe_parent src apply (clarsimp simp: is_simple_cap'_def sameRegionAs_def2 isCap_Master) apply (erule disjE) apply (clarsimp simp: ut_capRange_non_empty dest!: capMaster_capRange) apply clarsimp apply (clarsimp simp: safe_parent_for'_def) apply (erule disjE, clarsimp simp: isCap_simps) apply (clarsimp simp: isCap_simps capRange_def) done lemma ut_c'_new: assumes ut_src: "isUntypedCap src_cap" shows "m p = Some (CTE cap node) \ \ sameRegionAs c' cap" using src simple apply clarsimp apply (drule untyped_mdbD', rule ut_src, assumption) apply (clarsimp simp: is_simple_cap'_def sameRegionAs_def2 isCap_Master capRange_Master) apply (fastforce simp: isCap_simps) apply (frule sameRegion_capRange_sub) apply (drule ut_sameRegion_non_empty [OF ut_src]) apply (insert utCapRange_c') apply blast apply (rule untyped_mdb) apply (simp add: ut_descendants [OF ut_src]) done lemma c'_new: "m p = Some (CTE cap node) \ \ sameRegionAs c' cap" using safe_parent src unfolding safe_parent_for'_def apply (elim exE conjE) apply (erule disjE) apply (erule irq_c'_new [rotated]) apply (clarsimp simp: isCap_simps) apply clarsimp apply (drule (1) ut_c'_new) apply simp done lemma irq_control_src: "\ isIRQControlCap src_cap; m p = Some (CTE cap node); sameRegionAs cap c' \ \ p = src" using safe_parent src unfolding safe_parent_for'_def apply (clarsimp simp: isCap_simps) apply (clarsimp simp: sameRegionAs_def2 isCap_Master) apply (erule disjE, clarsimp simp: isCap_simps) apply (erule disjE, clarsimp simp: isCap_simps) apply (erule disjE, clarsimp simp: isCap_simps capRange_def) apply (clarsimp simp: isCap_simps) apply (drule (1) irq_controlD, rule irq_control) apply simp done lemma not_irq_parentD: "\ isIRQControlCap src_cap \ isUntypedCap src_cap \ descendants_of' src m = {} \ capRange c' \ {}" using src safe_parent unfolding safe_parent_for'_def by (clarsimp simp: isCap_simps) lemma ut_src_only_ut_c_parents: "\ isUntypedCap src_cap; sameRegionAs cap c'; m p = Some (CTE cap node) \ \ isUntypedCap cap" using safe_parent src unfolding safe_parent_for'_def apply clarsimp apply (erule disjE, clarsimp simp: isCap_simps) apply clarsimp apply (rule ccontr) apply (drule (3) untyped_mdbD') apply (frule sameRegion_capRange_sub) apply (insert utCapRange_c')[1] apply blast apply (rule untyped_mdb) apply simp done lemma ut_src: "\ isUntypedCap src_cap; sameRegionAs cap c'; m p = Some (CTE cap node) \ \ isUntypedCap cap \ untypedRange cap \ untypedRange src_cap \ {}" apply (frule (2) ut_src_only_ut_c_parents) apply simp apply (frule sameRegion_capRange_sub) apply (insert utCapRange_c')[1] apply (simp add: untypedCapRange) apply (drule ut_capRange_non_empty) apply blast done lemma chunked' [simp]: "mdb_chunked n'" using src dest apply (clarsimp simp: mdb_chunked_def) apply (drule n'_cap)+ apply (clarsimp simp: n'_trancl_eq) apply (clarsimp split: split_if_asm) prefer 3 apply (frule (3) mdb_chunkedD, rule chunked) apply clarsimp apply (rule conjI, clarsimp) apply (clarsimp simp: is_chunk_def n'_trancl_eq n_rtrancl_eq' n_dest' new_dest_def) apply (rule conjI, clarsimp) apply (rule conjI, clarsimp) apply clarsimp apply (erule_tac x=src in allE) apply simp apply (erule sameRegion_src_c') apply clarsimp apply (erule_tac x=p'' in allE) apply clarsimp apply (frule_tac p=p'' in m_cap') apply clarsimp apply clarsimp apply (clarsimp simp: is_chunk_def n'_trancl_eq n_rtrancl_eq' n_dest' new_dest_def) apply (rule conjI, clarsimp) apply (rule conjI, clarsimp) apply clarsimp apply (erule_tac x=src in allE) apply simp apply (erule sameRegion_src_c') apply clarsimp apply (erule_tac x=p'' in allE) apply clarsimp apply (frule_tac p=p'' in m_cap') apply clarsimp apply (case_tac "p' = src") apply simp apply (clarsimp simp: is_chunk_def) apply (simp add: n'_trancl_eq n_rtrancl_eq') apply (erule disjE) apply (simp add: n_dest' new_dest_def) apply clarsimp apply (drule (1) trancl_rtrancl_trancl) apply simp apply clarsimp apply (drule c'_new) apply (erule (1) notE) apply (case_tac "p=src") apply clarsimp apply (clarsimp simp: is_chunk_def) apply (simp add: n'_trancl_eq n_rtrancl_eq') apply (erule disjE) apply (clarsimp simp: n_dest' new_dest_def) apply clarsimp apply (drule (1) trancl_rtrancl_trancl) apply simp apply (case_tac "isIRQControlCap src_cap") apply (drule (2) irq_control_src) apply simp apply (drule not_irq_parentD) apply clarsimp apply (frule (2) ut_src) apply clarsimp apply (subgoal_tac "src \ descendants_of' p m") prefer 2 apply (drule (3) untyped_incD', rule untyped_inc) apply clarsimp apply fastforce apply (frule_tac m=m and p=p and p'=src in mdb_chunkedD, assumption+) apply (clarsimp simp: descendants_of'_def) apply (drule subtree_parent) apply (clarsimp simp: parentOf_def isMDBParentOf_def split: split_if_asm) apply simp apply (rule chunked) apply clarsimp apply (erule disjE) apply clarsimp apply (rule conjI) prefer 2 apply clarsimp apply (drule (1) trancl_trans, simp) apply (clarsimp simp: is_chunk_def) apply (simp add: n'_trancl_eq n_rtrancl_eq' split: split_if_asm) apply (clarsimp simp: n_dest' new_dest_def) apply (erule_tac x=p'' in allE) apply clarsimp apply (drule_tac p=p'' in m_cap') apply clarsimp apply clarsimp apply (rule conjI) apply clarsimp apply (drule (1) trancl_trans, simp) apply (clarsimp simp: descendants_of'_def) apply (drule subtree_mdb_next) apply (drule (1) trancl_trans) apply simp done lemma distinct_zombies_m: "distinct_zombies m" using valid by (simp add: valid_mdb_ctes_def) lemma untyped_rangefree: "\ isUntypedCap src_cap; m x = Some cte; x \ src; \ isUntypedCap (cteCap cte) \ \ capRange (cteCap cte) \ capRange c'" apply (frule ut_descendants) apply (cases cte, clarsimp) apply (frule(2) untyped_mdbD' [OF src _ _ _ _ untyped_mdb]) apply (simp add: untypedCapRange[symmetric]) apply (frule ut_capRange_non_empty) apply (cut_tac capRange_c') apply blast apply simp done lemma notZomb: "\ isZombie src_cap" "\ isZombie c'" using sameRegion_src simple by (auto simp: isCap_simps sameRegionAs_def3 simp del: sameRegion_src, auto simp: is_simple_cap'_def isCap_simps) lemma notArchPage: "\ isArchPageCap c'" using simple by (clarsimp simp: isCap_simps is_simple_cap'_def) lemma distinct_zombies[simp]: "distinct_zombies n'" using distinct_zombies_m apply (simp add: n'_def distinct_zombies_nonCTE_modify_map) apply (simp add: n_def modify_map_apply src dest) apply (rule distinct_zombies_sameE[rotated]) apply (simp add: src) apply simp+ apply (cases "isUntypedCap src_cap") apply (erule distinct_zombies_seperateE) apply (case_tac "y = src") apply (clarsimp simp add: src) apply (frule(3) untyped_rangefree) apply (simp add: capRange_def) apply (rule sameRegionAsE [OF sameRegion_src], simp_all) apply (erule distinct_zombies_copyMasterE, rule src) apply simp apply (simp add: notZomb) apply (simp add: notArchPage) apply (erule distinct_zombies_sameMasterE, rule dest) apply (clarsimp simp: isCap_simps) done lemma irq' [simp]: "irq_control n'" using simple apply (clarsimp simp: irq_control_def) apply (frule n'_cap) apply (drule n'_rev) apply (clarsimp split: split_if_asm) apply (simp add: is_simple_cap'_def) apply (frule irq_revocable, rule irq_control) apply clarsimp apply (drule n'_cap) apply (clarsimp split: split_if_asm) apply (erule disjE) apply (clarsimp simp: is_simple_cap'_def) apply (erule (1) irq_controlD, rule irq_control) done lemma reply_masters_rvk_fb: "reply_masters_rvk_fb m" using valid by (simp add: valid_mdb_ctes_def) lemma reply_masters_rvk_fb' [simp]: "reply_masters_rvk_fb n'" using reply_masters_rvk_fb simple apply (simp add: reply_masters_rvk_fb_def n'_def n_def ball_ran_modify_map_eq) apply (subst ball_ran_modify_map_eq) apply (clarsimp simp: modify_map_def m_p is_simple_cap'_def) apply (simp add: ball_ran_modify_map_eq m_p is_simple_cap'_def dest_cap isCap_simps) done lemma mdb: "valid_mdb_ctes n'" by (simp add: valid_mdb_ctes_def no_0_n' chain_n') end lemma updateCapFreeIndex_no_0: assumes preserve:"\m m'. mdb_inv_preserve m m' \ mdb_inv_preserve (Q m) (Q m')" shows "\\s. P (no_0(Q (ctes_of s))) \ cte_wp_at' (\c. c = srcCTE \ isUntypedCap (cteCap c)) src s\ updateCap src (capFreeIndex_update (\_. index) (cteCap srcCTE)) \\r s. P (no_0 (Q (ctes_of s)))\" apply (wp updateCap_ctes_of_wp) apply (subgoal_tac "mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\_. capFreeIndex_update (\_. index) (cteCap srcCTE)))))") apply (drule mdb_inv_preserve.by_products) apply simp apply (rule preserve) apply (simp add:cte_wp_at_ctes_of)+ apply (rule mdb_inv_preserve_updateCap) apply (clarsimp simp:cte_wp_at_ctes_of)+ done lemma setUntypedCapAsFull_no_0: assumes preserve:"\m m'. mdb_inv_preserve m m' \ mdb_inv_preserve (Q m) (Q m')" shows "\\s. P (no_0 (Q (ctes_of s))) \ cte_wp_at' (\c. c = srcCTE) src s\ setUntypedCapAsFull (cteCap srcCTE) cap src \\r s. P (no_0 (Q (ctes_of s)))\" apply (clarsimp simp:setUntypedCapAsFull_def split:if_splits,intro conjI impI) apply (wp updateCapFreeIndex_no_0) apply (clarsimp simp:preserve cte_wp_at_ctes_of)+ apply wp apply clarsimp done lemma cteInsert_simple_mdb': "\valid_mdb' and pspace_aligned' and pspace_distinct' and (\s. src \ dest) and K (capAligned cap) and (\s. safe_parent_for' (ctes_of s) src cap) and K (is_simple_cap' cap) \ cteInsert cap src dest \\_. valid_mdb'\" unfolding cteInsert_def valid_mdb'_def apply (fold revokable'_fold) apply simp apply (rule hoare_name_pre_state) apply (rule hoare_pre) apply (wp updateCap_ctes_of_wp getCTE_wp' setUntypedCapAsFull_ctes mdb_inv_preserve_updateCap mdb_inv_preserve_modify_map mdb_inv_preserve_update_cap_same | clarsimp)+ apply (clarsimp simp: cte_wp_at_ctes_of) apply (rule conjI) apply (clarsimp simp: valid_mdb_ctes_def) apply (case_tac cte) apply (rename_tac src_cap src_node) apply (case_tac ctea) apply (rename_tac dest_cap dest_node) apply clarsimp apply (subst modify_map_eq) apply simp+ apply (clarsimp simp:maskedAsFull_def is_simple_cap'_def) apply (subgoal_tac "mdb_insert_simple' (ctes_of sa) src src_cap src_node dest NullCap dest_node cap") prefer 2 apply (intro mdb_insert_simple'.intro mdb_insert_simple.intro mdb_insert_simple_axioms.intro mdb_ptr.intro mdb_insert.intro vmdb.intro mdb_ptr_axioms.intro mdb_insert_axioms.intro) apply (simp add:modify_map_def valid_mdb_ctes_maskedAsFull)+ apply (clarsimp simp:nullPointer_def)+ apply ((clarsimp simp:valid_mdb_ctes_def)+) apply (drule mdb_insert_simple'.mdb) apply (clarsimp simp:valid_mdb_ctes_def) done lemma cteInsert_valid_globals_simple: "\valid_global_refs' and (\s. safe_parent_for' (ctes_of s) src cap)\ cteInsert cap src dest \\rv. valid_global_refs'\" apply (simp add: cteInsert_def) apply (rule hoare_pre) apply (wp getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule (1) safe_parent_for_capRange_capBits) apply (drule (1) valid_global_refsD_with_objSize) apply (auto elim: order_trans[rotated]) done lemma cteInsert_simple_invs: "\invs' and cte_wp_at' (\c. cteCap c=NullCap) dest and valid_cap' cap and (\s. src \ dest) and (\s. safe_parent_for' (ctes_of s) src cap) and (\s. \irq. cap = IRQHandlerCap irq \ irq_issued' irq s) and ex_cte_cap_to' dest and K (is_simple_cap' cap)\ cteInsert cap src dest \\rv. invs'\" apply (rule hoare_pre) apply (simp add: invs'_def valid_state'_def valid_pspace'_def) apply (wp cur_tcb_lift sch_act_wf_lift valid_queues_lift tcb_in_cur_domain'_lift valid_irq_node_lift valid_queues_lift' irqs_masked_lift cteInsert_simple_mdb' cteInsert_valid_globals_simple cteInsert_norq | simp add: pred_tcb_at'_def)+ apply (auto simp: invs'_def valid_state'_def valid_pspace'_def elim: valid_capAligned) done lemma ensureEmptySlot_stronger [wp]: "\\s. cte_wp_at' (\c. cteCap c = NullCap) p s \ P s\ ensureEmptySlot p \\rv. P\, -" apply (simp add: ensureEmptySlot_def whenE_def unlessE_whenE) apply (wp getCTE_wp') apply (clarsimp simp: cte_wp_at'_def) done lemma lookupSlotForCNodeOp_real_cte_at'[wp]: "\valid_objs' and valid_cap' rootCap\ lookupSlotForCNodeOp isSrc rootCap cref depth \\rv. real_cte_at' rv\,-" apply (simp add: lookupSlotForCNodeOp_def split_def unlessE_def split del: split_if cong: if_cong) apply (rule hoare_pre) apply (wp resolveAddressBits_real_cte_at' | simp | wp_once hoare_drop_imps)+ done lemma cte_refs_maskCapRights[simp]: "cte_refs' (maskCapRights rghts cap) = cte_refs' cap" by (rule ext, cases cap, simp_all add: maskCapRights_def isCap_defs Let_def ArchRetype_H.maskCapRights_def split del: split_if split: arch_capability.split) lemma capASID_PageCap_None [simp]: "capASID (ArchObjectCap (PageCap r R page_size None)) = None" by (simp add: capASID_def) lemma getSlotCap_cap_to'[wp]: "\\\ getSlotCap cp \\rv s. \r\cte_refs' rv (irq_node' s). ex_cte_cap_to' r s\" apply (simp add: getSlotCap_def) apply (wp getCTE_wp) apply (fastforce simp: cte_wp_at_ctes_of ex_cte_cap_to'_def) done lemma getSlotCap_cap_to2: "\\ and K (\cap. P cap \ Q cap)\ getSlotCap slot \\rv s. P rv \ (\x \ cte_refs' rv (irq_node' s). ex_cte_cap_wp_to' Q x s)\" apply (simp add: getSlotCap_def) apply (wp getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of ex_cte_cap_wp_to'_def) apply fastforce done lemma locateSlot_cap_to'[wp]: "\\s. isCNodeCap cap \ (\r \ cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' P r s)\ locateSlotCNode (capCNodePtr cap) n (v && mask (capCNodeBits cap)) \ex_cte_cap_wp_to' P\" apply (simp add: locateSlot_conv) apply wp apply (clarsimp dest!: isCapDs valid_capAligned simp: objBits_simps mult.commute capAligned_def cte_level_bits_def) apply (erule bspec) apply (case_tac "bits < word_bits") apply simp apply (rule and_mask_less_size) apply (simp add: word_bits_def word_size) apply (simp add: power_overflow word_bits_def) done lemma rab_cap_to'': assumes P: "\cap. isCNodeCap cap \ P cap" shows "s \ \\s. isCNodeCap cap \ (\r\cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' P r s)\ resolveAddressBits cap cref depth \\rv s. ex_cte_cap_wp_to' P (fst rv) s\,\\\\" proof (induct arbitrary: s rule: resolveAddressBits.induct) case (1 cap fn cref depth) show ?case apply (subst resolveAddressBits.simps) apply (simp add: Let_def split_def cap_case_CNodeCap[unfolded isCap_simps] split del: split_if cong: if_cong) apply (rule hoare_pre_spec_validE) apply ((elim exE | wp_once spec_strengthen_postE[OF "1.hyps"])+, (rule refl conjI | simp add: in_monad split del: split_if del: cte_refs'.simps)+) apply (wp getSlotCap_cap_to2 | simp add: assertE_def split_def whenE_def locateSlotCap_def split del: split_if | simp add: imp_conjL[symmetric] | wp_once hoare_drop_imps)+ apply (clarsimp simp: P) done qed lemma rab_cap_to'[wp]: "\(\s. isCNodeCap cap \ (\r\cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' P r s)) and K (\cap. isCNodeCap cap \ P cap)\ resolveAddressBits cap cref depth \\rv s. ex_cte_cap_wp_to' P (fst rv) s\,-" apply (rule hoare_gen_asmE) apply (unfold validE_R_def) apply (rule use_spec, rule rab_cap_to'') apply simp done lemma lookupCNode_cap_to'[wp]: "\\s. \r\cte_refs' rootCap (irq_node' s). ex_cte_cap_to' r s\ lookupSlotForCNodeOp isSrc rootCap cref depth \\p. ex_cte_cap_to' p\,-" apply (simp add: lookupSlotForCNodeOp_def Let_def split_def unlessE_def split del: split_if cong: if_cong) apply (rule hoare_pre) apply (wp hoare_drop_imps | simp)+ done lemma badge_derived'_refl[simp]: "badge_derived' c c" by (simp add: badge_derived'_def) lemma derived'_not_Null: "\ is_derived' m p c capability.NullCap" "\ is_derived' m p capability.NullCap c" by (clarsimp simp: is_derived'_def badge_derived'_def)+ lemma getSlotCap_wp: "\\s. (\cap. cte_wp_at' (\c. cteCap c = cap) p s \ Q cap s)\ getSlotCap p \Q\" apply (simp add: getSlotCap_def) apply (wp getCTE_wp) apply (clarsimp simp: cte_wp_at'_def) done lemma storeWordUser_typ_at' : "\\s. P (typ_at' T p s)\ storeWordUser v w \\_ s. P (typ_at' T p s)\" unfolding storeWordUser_def by wp lemma arch_update_updateCap_invs: "\cte_wp_at' (is_arch_update' cap) p and invs' and valid_cap' cap\ updateCap p cap \\_. invs'\" apply (simp add: updateCap_def) apply (wp arch_update_setCTE_invs getCTE_wp') apply clarsimp done lemma updateCap_same_master: "\ cap_relation cap cap' \ \ corres dc (valid_objs and pspace_aligned and pspace_distinct and cte_wp_at (\c. cap_master_cap c = cap_master_cap cap \ \is_reply_cap c \ \is_master_reply_cap c \ \is_ep_cap c \ \is_ntfn_cap c) slot) (pspace_aligned' and pspace_distinct' and cte_at' (cte_map slot)) (set_cap cap slot) (updateCap (cte_map slot) cap')" (is "_ \ corres _ ?P ?P' _ _") apply (unfold updateCap_def) apply (rule corres_guard_imp) apply (rule_tac Q="?P" and R'="\cte. ?P' and (\s. ctes_of s (cte_map slot) = Some cte)" in corres_symb_exec_r_conj) apply (rule corres_stronger_no_failI) apply (rule no_fail_pre, wp) apply (clarsimp simp: cte_wp_at_ctes_of) apply clarsimp apply (clarsimp simp add: state_relation_def) apply (drule (1) pspace_relationsD) apply (frule (4) set_cap_not_quite_corres_prequel) apply (erule cte_wp_at_weakenE, rule TrueI) apply assumption apply assumption apply simp apply (rule refl) apply clarsimp apply (rule bexI) prefer 2 apply assumption apply (clarsimp simp: pspace_relations_def) apply (subst conj_assoc[symmetric]) apply (rule conjI) apply (frule setCTE_pspace_only) apply (clarsimp simp: set_cap_def in_monad split_def get_object_def set_object_def split: split_if_asm Structures_A.kernel_object.splits) apply (rule conjI) apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv) apply (intro allI conjI) apply (frule use_valid[OF _ setCTE_gsUserPages]) prefer 2 apply simp+ apply (frule use_valid[OF _ setCTE_gsCNodes]) prefer 2 apply simp+ apply (subst conj_assoc[symmetric]) apply (rule conjI) prefer 2 apply (rule conjI) prefer 2 apply (frule setCTE_pspace_only) apply clarsimp apply (clarsimp simp: set_cap_def in_monad split_def get_object_def set_object_def split: split_if_asm Structures_A.kernel_object.splits) apply (frule set_cap_caps_of_state_monad) apply (drule is_original_cap_set_cap) apply clarsimp apply (erule use_valid [OF _ setCTE_ctes_of_wp]) apply (clarsimp simp: revokable_relation_def simp del: fun_upd_apply) apply (clarsimp split: split_if_asm) apply (drule cte_map_inj_eq) prefer 2 apply (erule cte_wp_at_weakenE, rule TrueI) apply (simp add: null_filter_def split: split_if_asm) apply (erule cte_wp_at_weakenE, rule TrueI) apply (erule caps_of_state_cte_at) apply fastforce apply fastforce apply fastforce apply clarsimp apply (simp add: null_filter_def split: split_if_asm) apply (erule_tac x=aa in allE, erule_tac x=bb in allE) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (erule disjE) apply (clarsimp simp: cap_master_cap_simps dest!: cap_master_cap_eqDs) apply (case_tac rv) apply clarsimp apply (subgoal_tac "(aa,bb) \ slot") prefer 2 apply clarsimp apply (simp add: null_filter_def cte_wp_at_caps_of_state split: split_if_asm) apply (clarsimp simp: cdt_relation_def) apply (frule set_cap_caps_of_state_monad) apply (frule mdb_set_cap, frule exst_set_cap) apply clarsimp apply (erule use_valid [OF _ setCTE_ctes_of_wp]) apply (frule cte_wp_at_norm) apply (clarsimp simp del: fun_upd_apply) apply (frule (1) pspace_relation_ctes_ofI) apply fastforce apply fastforce apply (clarsimp simp del: fun_upd_apply) apply (subst same_master_descendants) apply assumption apply (clarsimp simp: master_cap_relation) apply (frule_tac d=c in master_cap_relation [symmetric], assumption) apply (frule is_reply_cap_relation[symmetric], drule is_reply_master_relation[symmetric])+ apply simp apply (drule masterCap.intro) apply (drule masterCap.isReplyCap) apply simp apply (drule is_ep_cap_relation)+ apply (drule master_cap_ep) apply simp apply (drule is_ntfn_cap_relation)+ apply (drule master_cap_ntfn) apply simp apply (simp add: in_set_cap_cte_at) apply(simp add: cdt_list_relation_def split del: split_if) apply(intro allI impI) apply(erule_tac x=aa in allE)+ apply(erule_tac x=bb in allE)+ apply(clarsimp split: split_if_asm) apply(case_tac rv, clarsimp) apply (wp getCTE_wp') apply clarsimp apply (rule no_fail_pre, wp) apply clarsimp apply assumption apply clarsimp apply (clarsimp simp: cte_wp_at_ctes_of) done lemma diminished_cte_refs': "diminished' cap cap' \ cte_refs' cap n = cte_refs' cap' n" by (clarsimp simp: diminished'_def) lemma diminished_Untyped' : "diminished' (UntypedCap r n x) cap = (cap = UntypedCap r n x)" apply (rule iffI) apply (case_tac cap) apply (clarsimp simp:isCap_simps maskCapRights_def diminished'_def split:split_if_asm)+ (* 6 subgoals *) apply (rename_tac arch_capability R) apply (case_tac arch_capability) apply (clarsimp simp: isCap_simps ArchRetype_H.maskCapRights_def maskCapRights_def diminished'_def Let_def)+ done lemma updateCapFreeIndex_valid_mdb_ctes: assumes preserve:"\m m'. mdb_inv_preserve m m' \ mdb_inv_preserve (Q m) (Q m')" and coin :"\m cte. \m src = Some cte\ \ (\cte'. (Q m) src = Some cte' \ cteCap cte = cteCap cte')" and assoc :"\m f. Q (modify_map m src (cteCap_update f)) = modify_map (Q m) src (cteCap_update f)" shows "\\s. usableUntypedRange (capFreeIndex_update (\_. index) cap) \ usableUntypedRange cap \ isUntypedCap cap \ valid_mdb_ctes (Q (ctes_of s)) \ cte_wp_at' (\c. cteCap c = cap) src s\ updateCap src (capFreeIndex_update (\_. index) cap) \\r s. (valid_mdb_ctes (Q (ctes_of s)))\" apply (wp updateCap_ctes_of_wp) apply (subgoal_tac "mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src (cteCap_update (\_. capFreeIndex_update (\_. index) cap))))") apply (clarsimp simp:valid_mdb_ctes_def) apply (intro conjI) apply ((simp add:mdb_inv_preserve.preserve_stuff mdb_inv_preserve.by_products)+)[7] apply (rule mdb_inv_preserve.untyped_inc') apply assumption apply (clarsimp simp:assoc cte_wp_at_ctes_of) apply (clarsimp simp:modify_map_def split:if_splits) apply (drule coin) apply clarsimp apply (erule(1) subsetD) apply simp apply (simp_all add:mdb_inv_preserve.preserve_stuff mdb_inv_preserve.by_products) apply (rule preserve) apply (clarsimp simp:cte_wp_at_ctes_of) apply (rule mdb_inv_preserve_updateCap) apply (clarsimp simp:cte_wp_at_ctes_of)+ done lemma updateFreeIndex_pspace': "\\s. (capFreeIndex cap \ idx \ idx \ 2 ^ capBlockSize cap \ is_aligned (of_nat idx :: word32) 4 \ isUntypedCap cap) \ valid_pspace' s \ cte_wp_at' (\c. cteCap c = cap) src s\ updateCap src (capFreeIndex_update (\_. idx) cap) \\r s. valid_pspace' s\" apply (clarsimp simp:valid_pspace'_def) apply (rule hoare_pre) apply (rule hoare_vcg_conj_lift) apply (clarsimp simp:updateCap_def) apply (wp getCTE_wp) apply (clarsimp simp:valid_mdb'_def) apply (wp updateCapFreeIndex_valid_mdb_ctes) apply (simp | wp)+ apply (clarsimp simp:cte_wp_at_ctes_of valid_mdb'_def) apply (case_tac cte,simp add:isCap_simps) apply (rename_tac capability mdbnode) apply (drule(1) ctes_of_valid_cap') apply (subgoal_tac "usableUntypedRange (capFreeIndex_update (\_. idx) capability) \ usableUntypedRange capability") apply (clarsimp simp:valid_cap'_def capAligned_def valid_untyped'_def simp del:atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff Int_atLeastAtMost atLeastatMost_empty_iff usableUntypedRange.simps split del:if_splits) apply (drule_tac x = ptr' in spec) apply (clarsimp simp:ko_wp_at'_def simp del:atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff Int_atLeastAtMost atLeastatMost_empty_iff usableUntypedRange.simps split del:if_splits) apply blast apply (clarsimp simp:isCap_simps valid_cap'_def capAligned_def split:if_splits) apply (erule order_trans[rotated]) apply (rule word_plus_mono_right) apply (rule of_nat_mono_maybe_le[THEN iffD1]) apply (subst word_bits_def[symmetric]) apply (erule less_le_trans[OF _ power_increasing]) apply simp apply simp apply (subst word_bits_def[symmetric]) apply (erule le_less_trans) apply (erule less_le_trans[OF _ power_increasing]) apply simp+ apply (erule is_aligned_no_wrap') apply (rule word_of_nat_less) apply simp done lemma updateFreeIndex_invs': "\\s. (capFreeIndex cap \ idx \ idx \ 2 ^ capBlockSize cap \ isUntypedCap cap \ is_aligned (of_nat idx :: word32) 4) \ invs' s \ cte_wp_at' (\c. cteCap c = cap) src s\ updateCap src (capFreeIndex_update (\_. idx) cap) \\r s. invs' s\" apply (clarsimp simp:invs'_def valid_state'_def) apply (wp updateFreeIndex_pspace' sch_act_wf_lift valid_queues_lift updateCap_iflive' tcb_in_cur_domain'_lift | simp add: pred_tcb_at'_def)+ apply (rule hoare_pre) apply (rule hoare_vcg_conj_lift) apply (simp add: ifunsafe'_def3 cteInsert_def setUntypedCapAsFull_def split del: split_if) apply (wp getCTE_wp) apply (rule hoare_vcg_conj_lift) apply (simp add:updateCap_def) apply wp apply (wp valid_irq_node_lift) apply (rule hoare_vcg_conj_lift) apply (simp add:updateCap_def) apply (wp setCTE_irq_handlers' getCTE_wp) apply (simp add:updateCap_def) apply (wp irqs_masked_lift valid_queues_lift' cur_tcb_lift ct_idle_or_in_cur_domain'_lift hoare_vcg_disj_lift) apply (clarsimp simp:cte_wp_at_ctes_of) apply (intro conjI allI impI) apply (clarsimp simp: modify_map_def cteCaps_of_def ifunsafe'_def3 split:if_splits) apply (drule_tac x=src in spec) apply (clarsimp simp:isCap_simps) apply (rule_tac x = cref' in exI) apply clarsimp apply (drule_tac x = cref in spec) apply clarsimp apply (rule_tac x = cref' in exI) apply clarsimp apply (drule(1) valid_global_refsD') apply (clarsimp simp: isCap_simps) apply (drule(1) valid_global_refsD_with_objSize) apply (clarsimp simp:isCap_simps cte_wp_at_ctes_of)+ done end