From 6cd14821691445972d9e9c229f17e1e8afe7b5be Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 25 Jun 2019 17:41:11 +1000 Subject: [PATCH] riscv refine: set up CSpace_I (0 sorries) --- proof/refine/RISCV64/CSpace_I.thy | 2044 +++++++++++++++++++++++++++++ 1 file changed, 2044 insertions(+) create mode 100644 proof/refine/RISCV64/CSpace_I.thy diff --git a/proof/refine/RISCV64/CSpace_I.thy b/proof/refine/RISCV64/CSpace_I.thy new file mode 100644 index 000000000..27e3a6dc3 --- /dev/null +++ b/proof/refine/RISCV64/CSpace_I.thy @@ -0,0 +1,2044 @@ +(* + * Copyright 2019, Data61, CSIRO + * + * 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(DATA61_GPL) + *) + +(* + CSpace invariants +*) + +theory CSpace_I +imports ArchAcc_R +begin + +hide_const span + +context begin interpretation Arch . (*FIXME: arch_split*) + +lemma capUntypedPtr_simps [simp]: + "capUntypedPtr (ThreadCap r) = r" + "capUntypedPtr (NotificationCap r badge a b) = r" + "capUntypedPtr (EndpointCap r badge a b c d) = r" + "capUntypedPtr (Zombie r bits n) = r" + "capUntypedPtr (ArchObjectCap x) = Arch.capUntypedPtr x" + "capUntypedPtr (UntypedCap d r n f) = r" + "capUntypedPtr (CNodeCap r n g n2) = r" + "capUntypedPtr (ReplyCap r m a) = r" + "Arch.capUntypedPtr (ASIDPoolCap r asid) = r" + "Arch.capUntypedPtr (FrameCap r rghts sz d mapdata) = r" + "Arch.capUntypedPtr (PageTableCap r mapdata2) = r" + by (auto simp: capUntypedPtr_def RISCV64_H.capUntypedPtr_def) + +lemma rights_mask_map_UNIV [simp]: + "rights_mask_map UNIV = allRights" + by (simp add: rights_mask_map_def allRights_def) + +declare insert_UNIV[simp] + +lemma maskCapRights_allRights [simp]: + "maskCapRights allRights c = c" + unfolding maskCapRights_def isCap_defs allRights_def + RISCV64_H.maskCapRights_def maskVMRights_def + by (cases c) (simp_all add: Let_def split: arch_capability.split vmrights.split) + +lemma diminished_refl'[simp]: + "diminished' cap cap" + unfolding diminished'_def + by (rule exI[where x=allRights], simp) + +lemma getCTE_inv [wp]: "\P\ getCTE addr \\rv. P\" + by (simp add: getCTE_def) wp + +lemma getEndpoint_inv [wp]: + "\P\ getEndpoint ptr \\rv. P\" + by (simp add: getEndpoint_def getObject_inv loadObject_default_inv) + +lemma getNotification_inv [wp]: + "\P\ getNotification ptr \\rv. P\" + by (simp add: getNotification_def getObject_inv loadObject_default_inv) + +lemma getSlotCap_inv [wp]: "\P\ getSlotCap addr \\rv. P\" + by (simp add: getSlotCap_def, wp) + +declare resolveAddressBits.simps[simp del] + +lemma cap_case_CNodeCap: + "(case cap of CNodeCap a b c d \ P + | _ \ Q) + = (if isCNodeCap cap then P else Q)" + by (cases cap, simp_all add: isCap_simps) + +lemma resolveAddressBits_inv_induct: + shows + "s \ \P\ + resolveAddressBits cap cref depth + \\rv. P\,\\rv. P\" +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: if_split 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: if_split)+) + apply (wp | simp add: locateSlot_conv split del: if_split + | wp (once) hoare_drop_imps)+ + done +qed + +lemma rab_inv' [wp]: + "\P\ resolveAddressBits cap addr depth \\rv. P\" + by (rule validE_valid, rule use_specE', rule resolveAddressBits_inv_induct) + +lemmas rab_inv'' [wp] = rab_inv' [folded resolveAddressBits_decl_def] + +crunch inv [wp]: lookupCap P + +lemma updateObject_cte_inv: + "\P\ updateObject (cte :: cte) ko x y n \\rv. P\" + apply (simp add: updateObject_cte) + apply (cases ko, simp_all add: typeError_def unless_def + split del: if_split + cong: if_cong) + apply (wp | simp)+ + done + +definition + "no_mdb cte \ mdbPrev (cteMDBNode cte) = 0 \ mdbNext (cteMDBNode cte) = 0" + +lemma mdb_next_update: + "m (x \ y) \ a \ b = + (if a = x then mdbNext (cteMDBNode y) = b else m \ a \ b)" + by (simp add: mdb_next_rel_def mdb_next_def) + +lemma neg_no_loopsI: + "m \ c \\<^sup>+ c \ \ no_loops m" + unfolding no_loops_def by auto + +lemma valid_dlistEp [elim?]: + "\ valid_dlist m; m p = Some cte; mdbPrev (cteMDBNode cte) \ 0; + \cte'. \ m (mdbPrev (cteMDBNode cte)) = Some cte'; + mdbNext (cteMDBNode cte') = p \ \ P \ \ + P" + unfolding valid_dlist_def Let_def by blast + +lemma valid_dlistEn [elim?]: + "\ valid_dlist m; m p = Some cte; mdbNext (cteMDBNode cte) \ 0; + \cte'. \ m (mdbNext (cteMDBNode cte)) = Some cte'; + mdbPrev (cteMDBNode cte') = p \ \ P \ \ + P" + unfolding valid_dlist_def Let_def by blast + +lemmas valid_dlistE = valid_dlistEn valid_dlistEp + +lemma mdb_next_update_other: + "\ m (x \ y) \ a \ b; x \ a \ \ m \ a \ b" + by (simp add: mdb_next_rel_def mdb_next_def) + +lemma mdb_trancl_update_other: + assumes upd: "m(p \ cte) \ x \\<^sup>+ y" + and nopath: "\ m \ x \\<^sup>* p" + shows "m \ x \\<^sup>+ y" + using upd nopath +proof induct + case (base y) + + have "m \ x \ y" + proof (rule mdb_next_update_other) + from base show "p \ x" by clarsimp + qed fact+ + + thus ?case .. +next + case (step y z) + hence ih: "m \ x \\<^sup>+ y" by auto + + from ih show ?case + proof + show "m \ y \ z" + proof (rule mdb_next_update_other) + show "p \ y" + proof (cases "x = p") + case True thus ?thesis using step.prems by simp + next + case False thus ?thesis using step.prems ih + by - (erule contrapos_nn, rule trancl_into_rtrancl, simp) + qed + qed fact+ + qed +qed + +lemma next_unfold': + "m \ c \ y = (\cte. m c = Some cte \ mdbNext (cteMDBNode cte) = y)" + unfolding mdb_next_rel_def + by (simp add: next_unfold split: option.splits) + +lemma no_self_loop_next_noloop: + assumes no_loop: "no_loops m" + and lup: "m ptr = Some cte" + shows "mdbNext (cteMDBNode cte) \ ptr" +proof - + from no_loop have "\ m \ ptr \ ptr" + unfolding no_loops_def + by - (drule spec, erule contrapos_nn, erule r_into_trancl) + + thus ?thesis using lup + by (simp add: next_unfold') +qed + + +lemma valid_dlistI [intro?]: + defines "nxt \ \cte. mdbNext (cteMDBNode cte)" + and "prv \ \cte. mdbPrev (cteMDBNode cte)" + assumes r1: "\p cte. \ m p = Some cte; prv cte \ 0 \ \ \cte'. m (prv cte) = Some cte' \ nxt cte' = p" + and r2: "\p cte. \ m p = Some cte; nxt cte \ 0 \ \ \cte'. m (nxt cte) = Some cte' \ prv cte' = p" + shows "valid_dlist m" + unfolding valid_dlist_def + by (auto dest: r1 r2 simp: Let_def prv_def nxt_def) + +lemma no_loops_tranclE: + assumes nl: "no_loops m" + and nxt: "m \ x \\<^sup>+ y" + shows "\ m \ y \\<^sup>* x" +proof + assume "m \ y \\<^sup>* x" + hence "m \ x \\<^sup>+ x" using nxt + by simp + + thus False using nl + unfolding no_loops_def by auto +qed + +lemma neg_next_rtrancl_trancl: + "\ \ m \ y \\<^sup>* r; m \ x \ y \ \ \ m \ x \\<^sup>+ r" + apply (erule contrapos_nn) + apply (drule tranclD) + apply (clarsimp simp: next_unfold') + done + +lemma next_trancl_split_tt: + assumes p1: "m \ x \\<^sup>+ y" + and p2: "m \ x \\<^sup>+ p" + and nm: "\ m \ p \\<^sup>* y" + shows "m \ y \\<^sup>* p" + using p2 p1 nm +proof induct + case base thus ?case + by (clarsimp dest!: tranclD) (drule (1) next_single_value, simp) +next + case (step q r) + + show ?case + proof (cases "q = y") + case True thus ?thesis using step + by fastforce + next + case False + have "m \ y \\<^sup>* q" + proof (rule step.hyps) + have "\ m \ q \\<^sup>+ y" + by (rule neg_next_rtrancl_trancl) fact+ + thus "\ m \ q \\<^sup>* y" using False + by (clarsimp dest!: rtranclD) + qed fact+ + thus ?thesis by (rule rtrancl_into_rtrancl) fact+ + qed +qed + +lemma no_loops_upd_last: + assumes noloop: "no_loops m" + and nxt: "m \ x \\<^sup>+ p" + shows "m (p \ cte) \ x \\<^sup>+ p" +proof - + from noloop nxt have xp: "x \ p" + by (clarsimp dest!: neg_no_loopsI) + + from nxt show ?thesis using xp + proof (induct rule: converse_trancl_induct') + case (base y) + hence "m (p \ cte) \ y \ p" using noloop + by (auto simp add: mdb_next_update) + thus ?case .. + next + case (step y z) + + from noloop step have xp: "z \ p" + by (clarsimp dest!: neg_no_loopsI) + + hence "m (p \ cte) \ y \ z" using step + by (simp add: mdb_next_update) + + moreover from xp have "m (p \ cte) \ z \\<^sup>+ p" using step.hyps assms + by (auto simp del: fun_upd_apply) + ultimately show ?case by (rule trancl_into_trancl2) + qed +qed + + +lemma no_0_neq [intro?]: + "\m c = Some cte; no_0 m\ \ c \ 0" + by (auto simp add: no_0_def) + +lemma no_0_update: + assumes no0: "no_0 m" + and pnz: "p \ 0" + shows "no_0 (m(p \ cte))" + using no0 pnz unfolding no_0_def by simp + +lemma has_loop_update: + assumes lp: "m(p \ cte) \ c \\<^sup>+ c'" + and cn0: "c' \ 0" + and mnext: "mdbNext (cteMDBNode cte) = 0" + and mn0: "no_0 m" + and pn0: "p \ 0" + shows "m \ c \\<^sup>+ c'" + using lp cn0 +proof induct + case (base y) + have "m \ c \ y" + proof (rule mdb_next_update_other) + show "p \ c" using base + by (clarsimp intro: contrapos_nn simp: mdb_next_update mnext) + qed fact+ + + thus ?case .. +next + case (step y z) + + show ?case + proof + have "y \ 0" by (rule no_0_lhs [OF _ no_0_update]) fact+ + thus "m \ c \\<^sup>+ y" using step by simp + next + have "z \ 0" by fact+ + hence "p \ y" using step.hyps mnext + by (clarsimp simp: mdb_next_update) + thus "m \ y \ z" + by (rule mdb_next_update_other [OF step.hyps(2)]) + qed +qed + +lemma mdb_rtrancl_update_other: + assumes upd: "m(p \ cte) \ x \\<^sup>* y" + and nopath: "\ m \ x \\<^sup>* p" + shows "m \ x \\<^sup>* y" + using upd +proof (cases rule: next_rtrancl_tranclE) + case eq thus ?thesis by simp +next + case trancl thus ?thesis + by (auto intro: trancl_into_rtrancl elim: mdb_trancl_update_other [OF _ nopath]) +qed + +lemma mdb_trancl_other_update: + assumes upd: "m \ x \\<^sup>+ y" + and np: "\ m \ x \\<^sup>* p" + shows "m(p \ cte) \ x \\<^sup>+ y" + using upd +proof induct + case (base q) + from np have "x \ p" by clarsimp + hence"m (p \ cte) \ x \ q" + using base by (simp add: mdb_next_update del: fun_upd_apply) + thus ?case .. +next + case (step q r) + + show ?case + proof + from step.hyps(1) np have "q \ p" + by (auto elim!: contrapos_nn) + + thus x: "m(p \ cte) \ q \ r" + using step by (simp add: mdb_next_update del: fun_upd_apply) + qed fact+ +qed + +lemma mdb_rtrancl_other_update: + assumes upd: "m \ x \\<^sup>* y" + and nopath: "\ m \ x \\<^sup>* p" + shows "m(p \ cte) \ x \\<^sup>* y" + using upd +proof (cases rule: next_rtrancl_tranclE) + case eq thus ?thesis by simp +next + case trancl thus ?thesis + by (auto intro: trancl_into_rtrancl elim: mdb_trancl_other_update [OF _ nopath]) +qed + +lemma mdb_chain_0_update: + assumes x: "m \ mdbNext (cteMDBNode cte) \\<^sup>* 0" + and np: "\ m \ mdbNext (cteMDBNode cte) \\<^sup>* p" + assumes p: "p \ 0" + assumes 0: "no_0 m" + assumes n: "mdb_chain_0 m" + shows "mdb_chain_0 (m(p \ cte))" + unfolding mdb_chain_0_def +proof rule + fix x + assume "x \ dom (m(p \ cte))" + hence x: "x = p \ x \ dom m" by simp + + have cnxt: "m(p \ cte) \ mdbNext (cteMDBNode cte) \\<^sup>* 0" + by (rule mdb_rtrancl_other_update) fact+ + + from x show "m(p \ cte) \ x \\<^sup>+ 0" + proof + assume xp: "x = p" + show ?thesis + proof (rule rtrancl_into_trancl2 [OF _ cnxt]) + show "m(p \ cte) \ x \ mdbNext (cteMDBNode cte)" using xp + by (simp add: mdb_next_update) + qed + next + assume x: "x \ dom m" + + show ?thesis + proof (cases "m \ x \\<^sup>* p") + case False + from n have "m \ x \\<^sup>+ 0" + unfolding mdb_chain_0_def + using x by auto + + thus ?thesis + by (rule mdb_trancl_other_update) fact+ + next + case True + hence "m(p \ cte) \ x \\<^sup>* p" + proof (cases rule: next_rtrancl_tranclE) + case eq thus ?thesis by simp + next + case trancl + have "no_loops m" by (rule mdb_chain_0_no_loops) fact+ + thus ?thesis + by (rule trancl_into_rtrancl [OF no_loops_upd_last]) fact+ + qed + moreover + have "m(p \ cte) \ p \ mdbNext (cteMDBNode cte)" by (simp add: mdb_next_update) + ultimately show ?thesis using cnxt by simp + qed + qed +qed + +lemma mdb_chain_0_update_0: + assumes x: "mdbNext (cteMDBNode cte) = 0" + assumes p: "p \ 0" + assumes 0: "no_0 m" + assumes n: "mdb_chain_0 m" + shows "mdb_chain_0 (m(p \ cte))" + using x 0 p + apply - + apply (rule mdb_chain_0_update [OF _ _ p 0 n]) + apply (auto elim: next_rtrancl_tranclE dest: no_0_lhs_trancl) + done + +lemma valid_badges_0_update: + assumes nx: "mdbNext (cteMDBNode cte) = 0" + assumes pv: "mdbPrev (cteMDBNode cte) = 0" + assumes p: "m p = Some cte'" + assumes m: "no_mdb cte'" + assumes 0: "no_0 m" + assumes d: "valid_dlist m" + assumes v: "valid_badges m" + shows "valid_badges (m(p \ cte))" +proof (unfold valid_badges_def, clarify) + fix c c' cap cap' n n' + assume c: "(m(p \ cte)) c = Some (CTE cap n)" + assume c': "(m(p \ cte)) c' = Some (CTE cap' n')" + assume nxt: "m(p \ cte) \ c \ c'" + assume r: "sameRegionAs cap cap'" + + from p 0 have p0: "p \ 0" by (clarsimp simp: no_0_def) + + from c' p0 0 + have "c' \ 0" by (clarsimp simp: no_0_def) + with nx nxt + have cp: "c \ p" by (clarsimp simp add: mdb_next_unfold) + moreover + from pv nx nxt p p0 c d m 0 + have "c' \ p" + apply clarsimp + apply (simp add: mdb_next_unfold split: if_split_asm) + apply (erule (1) valid_dlistEn, simp) + apply (clarsimp simp: no_mdb_def no_0_def) + done + moreover + with nxt c c' cp + have "m \ c \ c'" by (simp add: mdb_next_unfold) + ultimately + show "(isEndpointCap cap \ + capEPBadge cap \ capEPBadge cap' \ + capEPBadge cap' \ 0 \ + mdbFirstBadged n') \ + (isNotificationCap cap \ + capNtfnBadge cap \ capNtfnBadge cap' \ + capNtfnBadge cap' \ 0 \ + mdbFirstBadged n')" + using r c c' v by (fastforce simp: valid_badges_def) +qed + +definition + "caps_no_overlap' m S \ + \p c n. m p = Some (CTE c n) \ capRange c \ S = {}" + +definition + fresh_virt_cap_class :: "capclass \ cte_heap \ bool" +where + "fresh_virt_cap_class C m \ + C \ PhysicalClass \ C \ (capClass \ cteCap) ` ran m" + +lemma fresh_virt_cap_class_Physical[simp]: + "fresh_virt_cap_class PhysicalClass = \" + by (rule ext, simp add: fresh_virt_cap_class_def)+ + +lemma fresh_virt_cap_classD: + "\ m x = Some cte; fresh_virt_cap_class C m \ + \ C \ PhysicalClass \ capClass (cteCap cte) \ C" + by (auto simp: fresh_virt_cap_class_def) + +lemma capRange_untyped: + "capRange cap' \ untypedRange cap \ {} \ isUntypedCap cap" + by (cases cap, auto simp: isCap_simps) + +lemma capRange_of_untyped [simp]: + "capRange (UntypedCap d r n f) = untypedRange (UntypedCap d r n f)" + by (simp add: capRange_def isCap_simps capUntypedSize_def) + +lemma caps_contained_no_overlap: + "\ caps_no_overlap' m (capRange cap); caps_contained' m\ + \ caps_contained' (m(p \ CTE cap n))" + apply (clarsimp simp add: caps_contained'_def) + apply (rule conjI) + apply clarsimp + apply (rule conjI, clarsimp dest!: capRange_untyped) + apply clarsimp + apply (simp add: caps_no_overlap'_def) + apply (erule_tac x=p' in allE, erule allE, erule impE, erule exI) + apply (frule capRange_untyped) + apply (clarsimp simp add: isCap_simps) + apply clarsimp + apply (simp add: caps_no_overlap'_def) + apply (erule_tac x=pa in allE, erule allE, erule impE, erule exI) + apply (frule capRange_untyped) + apply (clarsimp simp: isCap_simps) + apply blast + done + +lemma no_mdb_next: + "\ m p = Some cte; no_mdb cte; valid_dlist m; no_0 m \ \ \ m \ x \ p" + apply clarsimp + apply (frule vdlist_nextD0) + apply clarsimp + apply assumption + apply (clarsimp simp: mdb_prev_def no_mdb_def mdb_next_unfold) + done + +lemma no_mdb_rtrancl: + "\ m p = Some cte; no_mdb cte; p \ x; valid_dlist m; no_0 m \ \ \ m \ x \\<^sup>* p" + apply (clarsimp dest!: rtranclD) + apply (drule tranclD2) + apply clarsimp + apply (drule (3) no_mdb_next) + apply fastforce + done + +lemma isNullCap [simp]: + "isNullCap cap = (cap = NullCap)" + by (simp add: isCap_simps) + +lemma isDomainCap [simp]: + "isDomainCap cap = (cap = DomainCap)" + by (simp add: isCap_simps) + +lemma isPhysicalCap[simp]: + "isPhysicalCap cap = (capClass cap = PhysicalClass)" + by (simp add: isPhysicalCap_def RISCV64_H.isPhysicalCap_def + split: capability.split arch_capability.split) + +definition capMasterCap :: "capability \ capability" where + "capMasterCap cap \ case cap of + EndpointCap ref bdg s r g gr \ EndpointCap ref 0 True True True True + | NotificationCap ref bdg s r \ NotificationCap ref 0 True True + | CNodeCap ref bits gd gs \ CNodeCap ref bits 0 0 + | ThreadCap ref \ ThreadCap ref + | ReplyCap ref master g \ ReplyCap ref True True + | UntypedCap d ref n f \ UntypedCap d ref n 0 + | ArchObjectCap acap \ ArchObjectCap (case acap of + FrameCap ref rghts sz d mapdata \ + FrameCap ref VMReadWrite sz d None + | ASIDPoolCap pool asid \ + ASIDPoolCap pool 0 + | PageTableCap ptr data \ + PageTableCap ptr None + | _ \ acap) + | _ \ cap" + +lemmas capMasterCap_simps[simp] = capMasterCap_def[split_simps capability.split arch_capability.split] + +lemma capMasterCap_eqDs1: + "capMasterCap cap = EndpointCap ref bdg s r g gr + \ bdg = 0 \ s \ r \ g \ gr + \ (\bdg s r g gr. cap = EndpointCap ref bdg s r g gr)" + "capMasterCap cap = NotificationCap ref bdg s r + \ bdg = 0 \ s \ r + \ (\bdg s r. cap = NotificationCap ref bdg s r)" + "capMasterCap cap = CNodeCap ref bits gd gs + \ gd = 0 \ gs = 0 \ (\gd gs. cap = CNodeCap ref bits gd gs)" + "capMasterCap cap = ThreadCap ref + \ cap = ThreadCap ref" + "capMasterCap cap = NullCap + \ cap = NullCap" + "capMasterCap cap = DomainCap + \ cap = DomainCap" + "capMasterCap cap = IRQControlCap + \ cap = IRQControlCap" + "capMasterCap cap = IRQHandlerCap irq + \ cap = IRQHandlerCap irq" + "capMasterCap cap = Zombie ref tp n + \ cap = Zombie ref tp n" + "capMasterCap cap = UntypedCap d ref bits 0 + \ \f. cap = UntypedCap d ref bits f" + "capMasterCap cap = ReplyCap ref master g + \ master \ g \ (\master g. cap = ReplyCap ref master g)" + "capMasterCap cap = ArchObjectCap (FrameCap ref rghts sz d mapdata) + \ rghts = VMReadWrite \ mapdata = None + \ (\rghts mapdata. cap = ArchObjectCap (FrameCap ref rghts sz d mapdata))" + "capMasterCap cap = ArchObjectCap ASIDControlCap + \ cap = ArchObjectCap ASIDControlCap" + "capMasterCap cap = ArchObjectCap (ASIDPoolCap pool asid) + \ asid = 0 \ (\asid. cap = ArchObjectCap (ASIDPoolCap pool asid))" + "capMasterCap cap = ArchObjectCap (PageTableCap ptr data) + \ data = None \ (\data. cap = ArchObjectCap (PageTableCap ptr data))" + by (clarsimp simp: capMasterCap_def + split: capability.split_asm arch_capability.split_asm)+ + +lemmas capMasterCap_eqDs[dest!] = capMasterCap_eqDs1 capMasterCap_eqDs1 [OF sym] + +definition + capBadge :: "capability \ machine_word option" +where + "capBadge cap \ if isEndpointCap cap then Some (capEPBadge cap) + else if isNotificationCap cap then Some (capNtfnBadge cap) + else None" + +lemma capBadge_simps[simp]: + "capBadge (UntypedCap d p n f) = None" + "capBadge (NullCap) = None" + "capBadge (DomainCap) = None" + "capBadge (EndpointCap ref badge s r g gr) = Some badge" + "capBadge (NotificationCap ref badge s r) = Some badge" + "capBadge (CNodeCap ref bits gd gs) = None" + "capBadge (ThreadCap ref) = None" + "capBadge (Zombie ref b n) = None" + "capBadge (ArchObjectCap cap) = None" + "capBadge (IRQControlCap) = None" + "capBadge (IRQHandlerCap irq) = None" + "capBadge (ReplyCap tcb master g) = None" + by (simp add: capBadge_def isCap_defs)+ + +lemma capClass_Master: + "capClass (capMasterCap cap) = capClass cap" + by (simp add: capMasterCap_def split: capability.split arch_capability.split) + +lemma capRange_Master: + "capRange (capMasterCap cap) = capRange cap" + by (simp add: capMasterCap_def split: capability.split arch_capability.split, + simp add: capRange_def) + +lemma master_eqI: + "\ \cap. F (capMasterCap cap) = F cap; F (capMasterCap cap) = F (capMasterCap cap') \ + \ F cap = F cap'" + by simp + +lemmas isArchFrameCap_simps[simp] = + isArchFrameCap_def[split_simps capability.split arch_capability.split] + +lemma isCap_Master: + "isZombie (capMasterCap cap) = isZombie cap" + "isArchObjectCap (capMasterCap cap) = isArchObjectCap cap" + "isThreadCap (capMasterCap cap) = isThreadCap cap" + "isCNodeCap (capMasterCap cap) = isCNodeCap cap" + "isNotificationCap (capMasterCap cap) = isNotificationCap cap" + "isEndpointCap (capMasterCap cap) = isEndpointCap cap" + "isUntypedCap (capMasterCap cap) = isUntypedCap cap" + "isReplyCap (capMasterCap cap) = isReplyCap cap" + "isIRQControlCap (capMasterCap cap) = isIRQControlCap cap" + "isIRQHandlerCap (capMasterCap cap) = isIRQHandlerCap cap" + "isNullCap (capMasterCap cap) = isNullCap cap" + "isDomainCap (capMasterCap cap) = isDomainCap cap" + "isArchFrameCap (capMasterCap cap) = isArchFrameCap cap" + by (simp add: isCap_simps capMasterCap_def + split: capability.split arch_capability.split)+ + +lemma capUntypedSize_capBits: + "capClass cap = PhysicalClass \ capUntypedSize cap = 2 ^ (capBits cap)" + apply (simp add: capUntypedSize_def objBits_simps' + RISCV64_H.capUntypedSize_def bit_simps' + split: capability.splits arch_capability.splits + zombie_type.splits) + apply fastforce + done + +lemma sameRegionAs_def2: + "sameRegionAs cap cap' = (\cap cap'. + (cap = cap' + \ (\ isNullCap cap \ \ isZombie cap + \ \ isUntypedCap cap \ \ isArchFrameCap cap) + \ (\ isNullCap cap' \ \ isZombie cap' + \ \ isUntypedCap cap' \ \ isArchFrameCap cap')) + \ (capRange cap' \ {} \ capRange cap' \ capRange cap + \ (isUntypedCap cap \ (isArchFrameCap cap \ isArchFrameCap cap'))) + \ (isIRQControlCap cap \ isIRQHandlerCap cap')) + (capMasterCap cap) (capMasterCap cap')" + apply (cases "isUntypedCap cap") + apply (clarsimp simp: sameRegionAs_def Let_def + isCap_Master capRange_Master capClass_Master) + apply (clarsimp simp: isCap_simps + capMasterCap_def[where cap="UntypedCap d p n f" for d p n f]) + apply (simp add: capRange_def capUntypedSize_capBits) + apply (intro impI iffI) + apply (clarsimp del: subsetI intro!: range_subsetI) + apply clarsimp + apply (simp cong: conj_cong) + apply (simp add: capMasterCap_def sameRegionAs_def isArchFrameCap_def + split: capability.split + split del: if_split cong: if_cong) + apply (simp add: RISCV64_H.sameRegionAs_def isCap_simps + split: arch_capability.split + split del: if_split cong: if_cong) + apply (clarsimp simp: capRange_def Let_def isCap_simps) + apply (simp add: range_subset_eq2 cong: conj_cong) + apply (simp add: conj_comms mask_def add_diff_eq) + done + +lemma sameObjectAs_def2: + "sameObjectAs cap cap' = (\cap cap'. + (cap = cap' + \ (\ isNullCap cap \ \ isZombie cap \ \ isUntypedCap cap) + \ (\ isNullCap cap' \ \ isZombie cap' \ \ isUntypedCap cap') + \ (isArchFrameCap cap \ capRange cap \ {}) + \ (isArchFrameCap cap' \ capRange cap' \ {}))) + (capMasterCap cap) (capMasterCap cap')" + apply (simp add: sameObjectAs_def sameRegionAs_def2 + isCap_simps capMasterCap_def + split: capability.split) + apply (clarsimp simp: RISCV64_H.sameObjectAs_def isCap_simps + split: arch_capability.split cong: if_cong) + apply (clarsimp simp: RISCV64_H.sameRegionAs_def isCap_simps + split del: if_split cong: if_cong) + apply (simp add: capRange_def isCap_simps mask_def add_diff_eq + split del: if_split) + apply fastforce + done + +lemmas sameRegionAs_def3 = + sameRegionAs_def2 [simplified capClass_Master capRange_Master isCap_Master] + +lemmas sameObjectAs_def3 = + sameObjectAs_def2 [simplified capClass_Master capRange_Master isCap_Master] + +lemma sameRegionAsE: + "\ sameRegionAs cap cap'; + \ capMasterCap cap = capMasterCap cap'; \ isNullCap cap; \ isZombie cap; + \ isUntypedCap cap; \ isArchFrameCap cap\ \ R; + \ capRange cap' \ {}; capRange cap' \ capRange cap; isUntypedCap cap \ \ R; + \ capRange cap' \ {}; capRange cap' \ capRange cap; isArchFrameCap cap; + isArchFrameCap cap' \ \ R; + \ isIRQControlCap cap; isIRQHandlerCap cap' \ \ R + \ \ R" + by (simp add: sameRegionAs_def3, fastforce) + +lemma sameObjectAsE: + "\ sameObjectAs cap cap'; + \ capMasterCap cap = capMasterCap cap'; \ isNullCap cap; \ isZombie cap; + \ isUntypedCap cap; + isArchFrameCap cap \ capRange cap \ {} \ \ R \ \ R" + by (clarsimp simp add: sameObjectAs_def3) + +lemma sameObjectAs_sameRegionAs: + "sameObjectAs cap cap' \ sameRegionAs cap cap'" + by (clarsimp simp add: sameObjectAs_def2 sameRegionAs_def2 isCap_simps) + +lemma sameObjectAs_sym: + "sameObjectAs c d = sameObjectAs d c" + by (simp add: sameObjectAs_def2 eq_commute conj_comms) + +lemma untypedRange_Master: + "untypedRange (capMasterCap cap) = untypedRange cap" + by (simp add: capMasterCap_def split: capability.split) + +lemma sameObject_capRange: + "sameObjectAs cap cap' \ capRange cap' = capRange cap" + apply (rule master_eqI, rule capRange_Master) + apply (clarsimp simp: sameObjectAs_def2) + done + +lemma sameRegionAs_Null [simp]: + "sameRegionAs c NullCap = False" + "sameRegionAs NullCap c = False" + by (simp add: sameRegionAs_def3 capRange_def isCap_simps)+ + +lemma isMDBParent_Null [simp]: + "isMDBParentOf c (CTE NullCap m) = False" + "isMDBParentOf (CTE NullCap m) c = False" + unfolding isMDBParentOf_def by (auto split: cte.splits) + +lemma capUntypedSize_simps [simp]: + "capUntypedSize (ThreadCap r) = 1 << objBits (undefined::tcb)" + "capUntypedSize (NotificationCap r badge a b) = 1 << objBits (undefined::Structures_H.notification)" + "capUntypedSize (EndpointCap r badge a b c d) = 1 << objBits (undefined::endpoint)" + "capUntypedSize (Zombie r zs n) = 1 << (zBits zs)" + "capUntypedSize NullCap = 0" + "capUntypedSize DomainCap = 1" + "capUntypedSize (ArchObjectCap x) = Arch.capUntypedSize x" + "capUntypedSize (UntypedCap d r n f) = 1 << n" + "capUntypedSize (CNodeCap r n g n2) = 1 << (objBits (undefined::cte) + n)" + "capUntypedSize (ReplyCap r m a) = 1 << objBits (undefined :: tcb)" + "capUntypedSize IRQControlCap = 1" + "capUntypedSize (IRQHandlerCap irq) = 1" + by (auto simp add: capUntypedSize_def isCap_simps objBits_simps' + split: zombie_type.splits) + +lemma sameRegionAs_classes: + "sameRegionAs cap cap' \ capClass cap = capClass cap'" + apply (erule sameRegionAsE) + apply (rule master_eqI, rule capClass_Master) + apply simp + apply (simp add: capRange_def split: if_split_asm) + apply (clarsimp simp: isCap_simps)+ + done + +lemma capAligned_capUntypedPtr: + "\ capAligned cap; capClass cap = PhysicalClass \ \ + capUntypedPtr cap \ capRange cap" + by (simp add: capRange_def capAligned_def is_aligned_no_overflow) + +lemma sameRegionAs_capRange_Int: + "\ sameRegionAs cap cap'; capClass cap = PhysicalClass \ capClass cap' = PhysicalClass; + capAligned cap; capAligned cap' \ + \ capRange cap' \ capRange cap \ {}" + apply (frule sameRegionAs_classes, simp) + apply (drule(1) capAligned_capUntypedPtr)+ + apply (erule sameRegionAsE) + apply (subgoal_tac "capRange (capMasterCap cap') \ capRange (capMasterCap cap) \ {}") + apply (simp(no_asm_use) add: capRange_Master) + apply (clarsimp simp: capRange_Master) + apply blast + apply blast + apply (clarsimp simp: isCap_simps) + done + +lemma sameRegionAs_trans: + "\ sameRegionAs a b; sameRegionAs b c \ \ sameRegionAs a c" + apply (simp add: sameRegionAs_def2, elim conjE disjE, simp_all) + by (auto simp: isCap_simps capRange_def) (* long *) + +lemma capMasterCap_maskCapRights[simp]: + "capMasterCap (maskCapRights msk cap) + = capMasterCap cap" + apply (cases cap; + simp add: maskCapRights_def Let_def isCap_simps capMasterCap_def) + apply (rename_tac arch_capability) + apply (case_tac arch_capability; + simp add: RISCV64_H.maskCapRights_def Let_def isCap_simps) + done + +lemma capBadge_maskCapRights[simp]: + "capBadge (maskCapRights msk cap) = capBadge cap" + apply (cases cap; + simp add: maskCapRights_def Let_def isCap_simps capBadge_def) + apply (rename_tac arch_capability) + apply (case_tac arch_capability; + simp add: RISCV64_H.maskCapRights_def Let_def isCap_simps) + done + +lemma getObject_cte_det: + "(r::cte,s') \ fst (getObject p s) \ fst (getObject p s) = {(r,s)} \ s' = s" + apply (clarsimp simp add: getObject_def bind_def get_def gets_def + return_def loadObject_cte split_def) + apply (clarsimp split: kernel_object.split_asm if_split_asm option.split_asm + simp: in_monad typeError_def alignError_def magnitudeCheck_def) + apply (simp_all add: bind_def return_def assert_opt_def split_def + alignCheck_def is_aligned_mask[symmetric] + unless_def when_def magnitudeCheck_def) + done + +lemma cte_wp_at_obj_cases': + "cte_wp_at' P p s = + (obj_at' P p s \ (\n \ dom tcb_cte_cases. obj_at' (P \ (fst (the (tcb_cte_cases n)))) (p - n) s))" + apply (simp add: cte_wp_at_cases' obj_at'_def) + apply (rule iffI) + apply (erule disjEI + | clarsimp simp: objBits_simps' cte_level_bits_def + | rule rev_bexI, erule domI)+ + apply fastforce + done + +lemma cte_wp_at_valid_objs_valid_cap': + "\ cte_wp_at' P p s; valid_objs' s \ \ \cte. P cte \ s \' (cteCap cte)" + apply (simp add: cte_wp_at_obj_cases') + apply (elim disjE bexE conjE) + apply (drule(1) obj_at_valid_objs') + apply (clarsimp simp: valid_obj'_def valid_cte'_def) + apply (drule(1) obj_at_valid_objs') + apply (clarsimp simp: valid_obj'_def valid_cte'_def valid_tcb'_def) + apply (fastforce dest: bspec [OF _ ranI]) + done + +lemma getCTE_valid_cap: + "\valid_objs'\ getCTE t \\cte s. s \' (cteCap cte) \ cte_at' t s\" + apply (clarsimp simp add: getCTE_def valid_def) + apply (frule in_inv_by_hoareD [OF getObject_cte_inv], clarsimp) + apply (subst conj_commute) + apply (subgoal_tac "cte_wp_at' ((=) a) t s") + apply (rule conjI) + apply (clarsimp elim!: cte_wp_at_weakenE') + apply (drule(1) cte_wp_at_valid_objs_valid_cap') + apply clarsimp + apply (drule getObject_cte_det) + apply (simp add: cte_wp_at'_def) + done + +lemmas getCTE_valid_cap' [wp] = + getCTE_valid_cap [THEN hoare_conjD1 [unfolded pred_conj_def]] + +lemma ctes_of_valid_cap': + "\ ctes_of s p = Some (CTE c n); valid_objs' s\ \ s \' c" + apply (rule cte_wp_at_valid_objs_valid_cap'[where P="(=) (CTE c n)", simplified]) + apply (simp add: cte_wp_at_ctes_of) + apply assumption + done + +lemma valid_capAligned: + "valid_cap' c s \ capAligned c" + by (simp add: valid_cap'_def) + +lemma caps_no_overlap'_no_region: + "\ caps_no_overlap' m (capRange cap); valid_objs' s; + m = ctes_of s; s \' cap; fresh_virt_cap_class (capClass cap) m \ \ + \c n p. m p = Some (CTE c n) \ + \ sameRegionAs c cap \ \ sameRegionAs cap c" + apply (clarsimp simp add: caps_no_overlap'_def) + apply (erule allE)+ + apply (erule impE, erule exI) + apply (frule (1) ctes_of_valid_cap') + apply (drule valid_capAligned)+ + apply (case_tac "capClass cap = PhysicalClass") + apply (auto dest: sameRegionAs_capRange_Int)[1] + apply (drule(1) fresh_virt_cap_classD) + apply (auto dest: sameRegionAs_classes) + done + +definition + "initMDBNode \ MDB nullPointer nullPointer True True" + +lemma init_next [simp]: + "mdbNext initMDBNode = 0" + by (simp add: initMDBNode_def nullPointer_def) + +lemma init_prev [simp]: + "mdbPrev initMDBNode = 0" + by (simp add: initMDBNode_def nullPointer_def) + +lemma mdb_chunked_init: + assumes x: "m x = Some cte" + assumes no_m: "no_mdb cte" + assumes no_c: "caps_no_overlap' m (capRange cap)" + assumes no_v: "fresh_virt_cap_class (capClass cap) m" + assumes no_0: "no_0 m" + assumes dlist: "valid_dlist m" + assumes chain: "mdb_chain_0 m" + assumes chunked: "mdb_chunked m" + assumes valid: "valid_objs' s" "m = ctes_of s" "s \' cap" + shows "mdb_chunked (m(x \ CTE cap initMDBNode))" + unfolding mdb_chunked_def +proof clarify + fix p p' c c' n n' + define m' where "m' \ m (x \ CTE cap initMDBNode)" + assume p: "m' p = Some (CTE c n)" + assume p': "m' p' = Some (CTE c' n')" + assume r: "sameRegionAs c c'" + assume neq: "p \ p'" + + note no_region = caps_no_overlap'_no_region [OF no_c valid no_v] + + from chain x no_0 + have chain': "mdb_chain_0 m'" + unfolding m'_def + apply - + apply (rule mdb_chain_0_update, clarsimp) + apply clarsimp + apply (drule rtranclD) + apply (erule disjE, clarsimp) + apply clarsimp + apply (drule tranclD) + apply (clarsimp simp: mdb_next_unfold) + apply clarsimp + apply assumption + apply assumption + done + moreover + from x no_0 + have x0 [simp]: "x \ 0" by clarsimp + with no_0 + have "no_0 m'" + unfolding m'_def + by (rule no_0_update) + ultimately + have nl: "no_loops m'" by (rule mdb_chain_0_no_loops) + + from p p' r neq no_region + have px: "p \ x" + by (clarsimp simp: m'_def) blast + moreover + from p p' r neq no_region + have p'x: "p' \ x" + by (clarsimp simp: m'_def) blast + ultimately + have m: + "(m \ p \\<^sup>+ p' \ m \ p' \\<^sup>+ p) \ + (m \ p \\<^sup>+ p' \ is_chunk m c p p') \ + (m \ p' \\<^sup>+ p \ is_chunk m c' p' p)" + using chunked p p' neq r + unfolding mdb_chunked_def m'_def + by simp + + from x no_m px [symmetric] dlist no_0 + have npx: "\ m \ p \\<^sup>* x" by (rule no_mdb_rtrancl) + + from x no_m p'x [symmetric] dlist no_0 + have np'x: "\ m \ p' \\<^sup>* x" by (rule no_mdb_rtrancl) + + show "(m' \ p \\<^sup>+ p' \ m' \ p' \\<^sup>+ p) \ + (m' \ p \\<^sup>+ p' \ is_chunk m' c p p') \ + (m' \ p' \\<^sup>+ p \ is_chunk m' c' p' p)" + proof (cases "m \ p \\<^sup>+ p'") + case True + with m + have ch: "is_chunk m c p p'" by simp + + from True npx + have "m' \ p \\<^sup>+ p'" + unfolding m'_def + by (rule mdb_trancl_other_update) + moreover + with nl + have "\ m' \ p' \\<^sup>+ p" + apply clarsimp + apply (drule (1) trancl_trans) + apply (simp add: no_loops_def) + done + moreover + have "is_chunk m' c p p'" + unfolding is_chunk_def + proof clarify + fix p'' + assume "m' \ p \\<^sup>+ p''" + with npx + have "m \ p \\<^sup>+ p''" + unfolding m'_def + by - (rule mdb_trancl_update_other) + moreover + then + have p''x: "p'' \ x" + using dlist x no_m no_0 + apply clarsimp + apply (drule tranclD2) + apply clarsimp + apply (frule vdlist_nextD0, simp, assumption) + apply (clarsimp simp: mdb_prev_def mdb_next_unfold no_mdb_def) + done + moreover + assume "m' \ p'' \\<^sup>* p'" + { + moreover + from x no_m p''x [symmetric] dlist no_0 + have "\m \ p'' \\<^sup>* x" by (rule no_mdb_rtrancl) + ultimately + have "m \ p'' \\<^sup>* p'" + unfolding m'_def + by (rule mdb_rtrancl_update_other) + } + ultimately + have "\cap'' n''. + m p'' = Some (CTE cap'' n'') \ sameRegionAs c cap''" + using ch + by (simp add: is_chunk_def) + with p''x + show "\cap'' n''. + m' p'' = Some (CTE cap'' n'') \ sameRegionAs c cap''" + by (simp add: m'_def) + qed + ultimately + show ?thesis by simp + next + case False + with m + have p'p: "m \ p' \\<^sup>+ p" by simp + with m + have ch: "is_chunk m c' p' p" by simp + from p'p np'x + have "m' \ p' \\<^sup>+ p" + unfolding m'_def + by (rule mdb_trancl_other_update) + moreover + with nl + have "\ m' \ p \\<^sup>+ p'" + apply clarsimp + apply (drule (1) trancl_trans) + apply (simp add: no_loops_def) + done + moreover + have "is_chunk m' c' p' p" + unfolding is_chunk_def + proof clarify + fix p'' + assume "m' \ p' \\<^sup>+ p''" + with np'x + have "m \ p' \\<^sup>+ p''" + unfolding m'_def + by - (rule mdb_trancl_update_other) + moreover + then + have p''x: "p'' \ x" + using dlist x no_m no_0 + apply clarsimp + apply (drule tranclD2) + apply clarsimp + apply (frule vdlist_nextD0, simp, assumption) + apply (clarsimp simp: mdb_prev_def mdb_next_unfold no_mdb_def) + done + moreover + assume "m' \ p'' \\<^sup>* p" + { + moreover + from x no_m p''x [symmetric] dlist no_0 + have "\m \ p'' \\<^sup>* x" by (rule no_mdb_rtrancl) + ultimately + have "m \ p'' \\<^sup>* p" + unfolding m'_def + by (rule mdb_rtrancl_update_other) + } + ultimately + have "\cap'' n''. + m p'' = Some (CTE cap'' n'') \ sameRegionAs c' cap''" + using ch + by (simp add: is_chunk_def) + with p''x + show "\cap'' n''. + m' p'' = Some (CTE cap'' n'') \ sameRegionAs c' cap''" + by (simp add: m'_def) + qed + ultimately + show ?thesis by simp + qed +qed + +lemma cte_refs_capRange: + "\ s \' c; \irq. c \ IRQHandlerCap irq \ \ cte_refs' c x \ capRange c" + apply (cases c; simp add: capRange_def isCap_simps) + apply (clarsimp dest!: valid_capAligned + simp: capAligned_def objBits_simps field_simps) + apply (frule tcb_cte_cases_small) + apply (intro conjI) + apply (erule(1) is_aligned_no_wrap') + apply (rule word_plus_mono_right[where z="2^tcbBlockSizeBits - 1", simplified field_simps]) + apply (drule minus_one_helper3, simp) + apply (erule is_aligned_no_wrap'[where off="2^tcbBlockSizeBits - 1", simplified field_simps]) + apply (drule minus_one_helper3) + apply simp + defer + \ \CNodeCap\ + apply (clarsimp simp: objBits_simps capAligned_def dest!: valid_capAligned) + apply (rename_tac word1 nat1 word2 nat2 x) + apply (subgoal_tac "x * 2^cteSizeBits < 2 ^ (cteSizeBits + nat1)") + apply (intro conjI) + apply (simp add: shiftl_t2n mult_ac) + apply (erule(1) is_aligned_no_wrap') + apply (simp add: add_diff_eq[symmetric]) + apply (rule word_plus_mono_right) + apply simp + apply (simp add: shiftl_t2n mult_ac) + apply (erule is_aligned_no_wrap') + apply simp + apply (simp add: power_add field_simps mask_def) + apply (erule word_mult_less_mono1) + apply (simp add: objBits_defs) + apply (frule power_strict_increasing [where a="2 :: nat" and n="y + z" for y z]) + apply simp + apply (simp only: power_add) + apply (simp add: word_bits_def) + \ \Zombie\ + apply (rename_tac word zombie_type nat) + apply (clarsimp simp: capAligned_def valid_cap'_def objBits_simps) + apply (subgoal_tac "xa * 2^cteSizeBits < 2 ^ zBits zombie_type") + apply (intro conjI) + apply (simp add: shiftl_t2n mult_ac) + apply (erule(1) is_aligned_no_wrap') + apply (simp add: add_diff_eq[symmetric]) + apply (rule word_plus_mono_right) + apply (simp add: shiftl_t2n mult_ac) + apply (erule is_aligned_no_wrap') + apply simp + apply (case_tac zombie_type) + apply simp + apply (rule div_lt_mult) + apply (simp add: objBits_defs) + apply (erule order_less_le_trans) + apply (simp add: word_le_nat_alt) + apply (subst le_unat_uoi[where z=5]) + apply simp + apply simp + apply (simp add: objBits_defs) + apply (simp add: objBits_simps' power_add mult.commute) + apply (rule word_mult_less_mono1) + apply (erule order_less_le_trans) + apply (simp add: word_le_nat_alt) + apply (subst le_unat_uoi) + apply (subst unat_power_lower) + prefer 2 + apply assumption + apply (simp add: word_bits_def) + apply (simp add: word_bits_def) + apply simp + apply (frule power_strict_increasing [where a="2 :: nat" and n="y + z" for y z]) + apply simp + apply (simp only: power_add) + apply (simp add: word_bits_def) + done + +lemma untypedCapRange: + "isUntypedCap cap \ capRange cap = untypedRange cap" + by (clarsimp simp: isCap_simps) + +lemma no_direct_loop [simp]: + "no_loops m \ m (mdbNext node) \ Some (CTE cap node)" + by (fastforce simp: mdb_next_rel_def mdb_next_def no_loops_def) + +lemma no_loops_direct_simp: + "no_loops m \ m \ x \ x = False" + by (auto simp add: no_loops_def) + +lemma no_loops_trancl_simp: + "no_loops m \ m \ x \\<^sup>+ x = False" + by (auto simp add: no_loops_def) + +lemma subtree_mdb_next: + "m \ a \ b \ m \ a \\<^sup>+ b" + by (erule subtree.induct) (auto simp: mdb_next_rel_def intro: trancl_into_trancl) +end + +context mdb_order +begin + +lemma no_loops: "no_loops m" + using chain no_0 by (rule mdb_chain_0_no_loops) + +lemma irrefl_direct_simp [iff]: + "m \ x \ x = False" + using no_loops by (rule no_loops_direct_simp) + +lemma irrefl_trancl_simp [iff]: + "m \ x \\<^sup>+ x = False" + using no_loops by (rule no_loops_trancl_simp) + +lemma irrefl_subtree [iff]: + "m \ x \ x = False" + by (clarsimp dest!: subtree_mdb_next) + +end (* of context mdb_order *) + +lemma no_loops_prev_next_0: + fixes m :: cte_heap + assumes src: "m src = Some (CTE src_cap src_node)" + assumes no_loops: "no_loops m" + assumes dlist: "valid_dlist m" + shows "(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 blast +qed + +lemma no_loops_next_prev_0: + fixes m :: cte_heap + assumes "m src = Some (CTE src_cap src_node)" + assumes "no_loops m" + assumes "valid_dlist m" + shows "(mdbNext src_node = mdbPrev src_node) = + (mdbPrev src_node = 0 \ mdbNext src_node = 0)" + apply (rule iffI) + apply (drule sym) + apply (simp add: no_loops_prev_next_0 [OF assms]) + apply clarsimp + done + +locale vmdb = mdb_next + + assumes valid: "valid_mdb_ctes m" + +sublocale vmdb < mdb_order + using valid + by (auto simp: greater_def greater_eq_def mdb_order_def valid_mdb_ctes_def) + +context vmdb +begin + +declare no_0 [intro!] +declare no_loops [intro!] + +lemma dlist [intro!]: "valid_dlist m" + using valid by (simp add: valid_mdb_ctes_def) + +lemmas m_0_simps [iff] = no_0_simps [OF no_0] + +lemma prev_next_0_p: + assumes "m p = Some (CTE cap node)" + shows "(mdbPrev node = mdbNext node) = + (mdbPrev node = 0 \ mdbNext node = 0)" + using assms by (rule no_loops_prev_next_0) auto + +lemma next_prev_0_p: + assumes "m p = Some (CTE cap node)" + shows "(mdbNext node = mdbPrev node) = + (mdbPrev node = 0 \ mdbNext node = 0)" + using assms by (rule no_loops_next_prev_0) auto + +lemmas dlistEn = valid_dlistEn [OF dlist] +lemmas dlistEp = valid_dlistEp [OF dlist] + +lemmas dlist_prevD = vdlist_prevD [OF _ _ dlist no_0] +lemmas dlist_nextD = vdlist_nextD [OF _ _ dlist no_0] +lemmas dlist_prevD0 = vdlist_prevD0 [OF _ _ dlist] +lemmas dlist_nextD0 = vdlist_nextD0 [OF _ _ dlist] +lemmas dlist_prev_src_unique = vdlist_prev_src_unique [OF _ _ _ dlist] +lemmas dlist_next_src_unique = vdlist_next_src_unique [OF _ _ _ dlist] + +lemma subtree_not_0 [simp]: + "\m \ p \ 0" + apply clarsimp + apply (erule subtree.cases) + apply auto + done + +lemma not_0_subtree [simp]: + "\m \ 0 \ p" + apply clarsimp + apply (erule subtree.induct) + apply (auto simp: mdb_next_unfold) + done + +lemma not_0_next [simp]: + "\ m \ 0 \ p" + by (clarsimp simp: mdb_next_unfold) + +lemma not_0_trancl [simp]: + "\ m \ 0 \\<^sup>+ p" + by (clarsimp dest!: tranclD) + +lemma rtrancl0 [simp]: + "m \ 0 \\<^sup>* p = (p = 0)" + by (auto dest!: rtranclD) + +lemma valid_badges: "valid_badges m" + using valid by (simp add: valid_mdb_ctes_def) + +lemma nullcaps: "valid_nullcaps m" + using valid by (simp add: valid_mdb_ctes_def) + +lemma + caps_contained: "caps_contained' m" and + chunked: "mdb_chunked m" and + untyped_mdb: "untyped_mdb' m" and + untyped_inc: "untyped_inc' m" and + class_links: "class_links m" and + irq_control: "irq_control m" + using valid by (simp add: valid_mdb_ctes_def)+ + +end (* of context vmdb *) + +lemma no_self_loop_next: + assumes vmdb: "valid_mdb_ctes m" + and lup: "m ptr = Some cte" + shows "mdbNext (cteMDBNode cte) \ ptr" +proof - + from vmdb have "no_loops m" .. + thus ?thesis + by (rule no_self_loop_next_noloop) fact+ +qed + +lemma no_self_loop_prev: + assumes vmdb: "valid_mdb_ctes m" + and lup: "m ptr = Some cte" + shows "mdbPrev (cteMDBNode cte) \ ptr" +proof + assume prev: "mdbPrev (cteMDBNode cte) = ptr" + + from vmdb have "no_0 m" .. + with lup have "ptr \ 0" + by (rule no_0_neq) + + moreover have "mdbNext (cteMDBNode cte) \ ptr" + by (rule no_self_loop_next) fact+ + + moreover from vmdb have "valid_dlist m" .. + + ultimately show False using lup prev + by - (erule (1) valid_dlistEp, simp_all) +qed + + +locale mdb_ptr = vmdb + + fixes p cap node + assumes m_p [intro!]: "m p = Some (CTE cap node)" +begin + +lemma p_not_next [simp]: + "(p = mdbNext node) = False" + using valid m_p by (fastforce dest: no_self_loop_next) + +lemma p_not_prev [simp]: + "(p = mdbPrev node) = False" + using valid m_p by (fastforce dest: no_self_loop_prev) + +lemmas next_not_p [simp] = p_not_next [THEN x_sym] +lemmas prev_not_p [simp] = p_not_prev [THEN x_sym] + +lemmas prev_next_0 [simp] = prev_next_0_p [OF m_p] next_prev_0_p [OF m_p] + +lemma p_0 [simp]: "p \ 0" using m_p by clarsimp + +lemma p_nextD: + assumes p': "m p' = Some (CTE cap' node')" + assumes eq: "mdbNext node = mdbNext node'" + shows "p = p' \ mdbNext node = 0 \ mdbNext node' = 0" +proof (cases "mdbNext node = 0") + case True thus ?thesis using eq by simp +next + case False + with eq have n': "mdbNext node' \ 0" by simp + + have "p = p'" + apply (rule dlistEn [OF m_p, simplified, OF False]) + apply (simp add: eq) + apply (rule dlistEn [OF p', simplified, OF n']) + apply clarsimp + done + + thus ?thesis by blast +qed + +lemma p_next_eq: + assumes "m p' = Some (CTE cap' node')" + shows "(mdbNext node = mdbNext node') = + (p = p' \ mdbNext node = 0 \ mdbNext node' = 0)" + using assms m_p + apply - + apply (rule iffI) + apply (erule (1) p_nextD) + apply auto + done + +lemma p_prevD: + assumes p': "m p' = Some (CTE cap' node')" + assumes eq: "mdbPrev node = mdbPrev node'" + shows "p = p' \ mdbPrev node = 0 \ mdbPrev node' = 0" +proof (cases "mdbPrev node = 0") + case True thus ?thesis using eq by simp +next + case False + with eq have n': "mdbPrev node' \ 0" by simp + + have "p = p'" + apply (rule dlistEp [OF m_p, simplified, OF False]) + apply (simp add: eq) + apply (rule dlistEp [OF p', simplified, OF n']) + apply clarsimp + done + + thus ?thesis by blast +qed + +lemma p_prev_eq: + assumes "m p' = Some (CTE cap' node')" + shows "(mdbPrev node = mdbPrev node') = + (p = p' \ mdbPrev node = 0 \ mdbPrev node' = 0)" + using assms m_p + apply - + apply (rule iffI) + apply (erule (1) p_prevD) + apply auto + done + +lemmas p_prev_qe = p_prev_eq [THEN x_sym] +lemmas p_next_qe = p_next_eq [THEN x_sym] + +lemma m_p_prev [intro!]: + "m \ mdbPrev node \ p" + using m_p by (clarsimp simp: mdb_prev_def) + +lemma m_p_next [intro!]: + "m \ p \ mdbNext node" + using m_p by (clarsimp simp: mdb_next_unfold) + +lemma next_p_prev: + "mdbNext node \ 0 \ m \ p \ mdbNext node" + by (rule dlist_nextD0 [OF m_p_next]) + +lemma prev_p_next: + "mdbPrev node \ 0 \ m \ mdbPrev node \ p" + by (rule dlist_prevD0 [OF m_p_prev]) + +lemma p_next: + "(m \ p \ p') = (p' = mdbNext node)" + using m_p by (auto simp: mdb_next_unfold) + +end (* of locale mdb_ptr *) + +lemma no_mdb_not_target: + "\ m \ c \ c'; m p = Some cte; no_mdb cte; valid_dlist m; no_0 m \ + \ c' \ p" + apply clarsimp + apply (subgoal_tac "c \ 0") + prefer 2 + apply (clarsimp simp: mdb_next_unfold) + apply (drule (3) vdlist_nextD) + apply (clarsimp simp: mdb_prev_def) + apply (simp add: no_mdb_def) + done + +context begin interpretation Arch . (*FIXME: arch_split*) +lemma valid_dlist_init: + "\ valid_dlist m; m p = Some cte; no_mdb cte \ \ + valid_dlist (m (p \ CTE cap initMDBNode))" + apply (simp add: initMDBNode_def Let_def nullPointer_def) + apply (clarsimp simp: no_mdb_def valid_dlist_def Let_def) + apply fastforce + done +end + +lemma (in mdb_ptr) descendants_of_init': + assumes n: "no_mdb (CTE cap node)" + shows + "descendants_of' p' (m(p \ CTE c initMDBNode)) = + descendants_of' p' m" + apply (rule set_eqI) + apply (simp add: descendants_of'_def) + apply (rule iffI) + apply (erule subtree.induct) + apply (frule no_mdb_not_target [where p=p]) + apply simp + apply (simp add: no_mdb_def) + apply (rule valid_dlist_init[OF dlist, OF m_p n]) + apply (insert no_0)[1] + apply (clarsimp simp: no_0_def) + apply (clarsimp simp: mdb_next_unfold split: if_split_asm) + apply (rule direct_parent) + apply (clarsimp simp: mdb_next_unfold) + apply assumption + apply (clarsimp simp: parentOf_def split: if_split_asm) + apply (frule no_mdb_not_target [where p=p]) + apply simp + apply (simp add: no_mdb_def) + apply (rule valid_dlist_init[OF dlist, OF m_p n]) + apply (insert no_0)[1] + apply (clarsimp simp: no_0_def) + apply (subgoal_tac "p' \ p") + apply (erule trans_parent) + apply (clarsimp simp: mdb_next_unfold split: if_split_asm) + apply assumption + apply (clarsimp simp: parentOf_def m_p split: if_split_asm) + apply clarsimp + apply (drule subtree_mdb_next)+ + apply (drule tranclD)+ + apply clarsimp + apply (insert n)[1] + apply (clarsimp simp: mdb_next_unfold m_p no_mdb_def) + apply (erule subtree.induct) + apply (frule no_mdb_not_target [where p=p], rule m_p, rule n) + apply (rule dlist) + apply (rule no_0) + apply (subgoal_tac "p'\p") + prefer 2 + apply (insert n)[1] + apply (clarsimp simp: mdb_next_unfold m_p no_mdb_def) + apply (rule direct_parent) + apply (clarsimp simp: mdb_next_unfold) + apply assumption + apply (clarsimp simp: parentOf_def) + apply (frule no_mdb_not_target [where p=p], rule m_p, rule n) + apply (rule dlist) + apply (rule no_0) + apply (subgoal_tac "c'\p") + prefer 2 + apply (insert n)[1] + apply (clarsimp simp: mdb_next_unfold m_p no_mdb_def) + apply (subgoal_tac "p'\p") + apply (erule trans_parent) + apply (clarsimp simp: mdb_next_unfold) + apply assumption + apply (clarsimp simp: parentOf_def) + apply clarsimp + apply (drule subtree_mdb_next) + apply (drule tranclD) + apply clarsimp + apply (insert n) + apply (clarsimp simp: mdb_next_unfold no_mdb_def m_p) + done + +lemma untyped_mdb_init: + "\ valid_mdb_ctes m; m p = Some cte; no_mdb cte; + caps_no_overlap' m (capRange cap); untyped_mdb' m; + valid_objs' s; s \' cap; + m = ctes_of s\ + \ untyped_mdb' (m(p \ CTE cap initMDBNode))" + apply (clarsimp simp add: untyped_mdb'_def) + apply (rule conjI) + apply clarsimp + apply (simp add: caps_no_overlap'_def) + apply (erule_tac x=p' in allE, erule allE, erule impE, erule exI) + apply (drule (1) ctes_of_valid_cap')+ + apply (drule valid_capAligned)+ + apply (drule untypedCapRange)+ + apply simp + apply (cases cte) + apply (rename_tac capability mdbnode) + apply clarsimp + apply (subgoal_tac "mdb_ptr (ctes_of s) p capability mdbnode") + prefer 2 + apply (simp add: vmdb_def mdb_ptr_def mdb_ptr_axioms_def) + apply (clarsimp simp: mdb_ptr.descendants_of_init') + apply (simp add: caps_no_overlap'_def) + apply (erule_tac x=pa in allE, erule allE, erule impE, erule exI) + apply (drule (1) ctes_of_valid_cap')+ + apply (drule valid_capAligned untypedCapRange)+ + apply simp + apply blast + done + +lemma aligned_untypedRange_non_empty: + "\capAligned c; isUntypedCap c\ \ untypedRange c \ {}" + apply (frule untypedCapRange) + apply (drule capAligned_capUntypedPtr) + apply (clarsimp simp: isCap_simps) + apply blast + done + +lemma untypedRange_not_emptyD: "untypedRange c' \ {} \ isUntypedCap c'" + by (case_tac c'; simp add: isCap_simps) + +lemma usableRange_subseteq: + "\capAligned c';isUntypedCap c'\ \ usableUntypedRange c' \ untypedRange c'" + apply (clarsimp simp:isCap_simps capAligned_def mask_def add_diff_eq split:if_splits) + apply (erule order_trans[OF is_aligned_no_wrap']) + apply (erule of_nat_power) + apply (simp add:word_bits_def)+ + done + +lemma untypedRange_in_capRange: "untypedRange x \ capRange x" + by (case_tac x; simp add: capRange_def) + +lemma untyped_inc_init: + "\ valid_mdb_ctes m; m p = Some cte; no_mdb cte; + caps_no_overlap' m (capRange cap); + valid_objs' s; s \' cap; + m = ctes_of s\ + \ untyped_inc' (m(p \ CTE cap initMDBNode))" + apply (clarsimp simp add: valid_mdb_ctes_def untyped_inc'_def) + apply (intro conjI impI) + apply clarsimp + apply (simp add: caps_no_overlap'_def) + apply (erule_tac x=p' in allE, erule allE, erule impE, erule exI) + apply (drule (1) ctes_of_valid_cap')+ + apply (drule valid_capAligned)+ + apply (frule usableRange_subseteq[OF _ untypedRange_not_emptyD]) + apply (drule (1) aligned_untypedRange_non_empty) + apply assumption + apply (frule_tac c' = c' in usableRange_subseteq) + apply (drule (1) aligned_untypedRange_non_empty) + apply assumption + apply (drule(1) aligned_untypedRange_non_empty)+ + apply (thin_tac "All P" for P) + apply (subgoal_tac "untypedRange cap \ untypedRange c' = {}") + apply (intro conjI) + apply simp + apply (drule(2) set_inter_not_emptyD2) + apply fastforce + apply (drule(2) set_inter_not_emptyD1) + apply fastforce + apply (drule(2) set_inter_not_emptyD3) + apply simp+ + apply (rule disjoint_subset2[OF _ disjoint_subset]) + apply (rule untypedRange_in_capRange)+ + apply (simp add:Int_ac) + apply clarsimp + apply (cases cte) + apply (rename_tac capability mdbnode) + apply clarsimp + apply (subgoal_tac "mdb_ptr (ctes_of s) p capability mdbnode") + prefer 2 + apply (simp add: vmdb_def mdb_ptr_def mdb_ptr_axioms_def valid_mdb_ctes_def untyped_inc'_def) + apply (clarsimp simp: mdb_ptr.descendants_of_init') + apply (simp add: caps_no_overlap'_def) + apply (erule_tac x=pa in allE, erule allE, erule impE, erule exI) + apply (drule (1) ctes_of_valid_cap')+ + apply (drule valid_capAligned)+ + apply (frule usableRange_subseteq[OF _ untypedRange_not_emptyD]) + apply (drule (1) aligned_untypedRange_non_empty) + apply assumption + apply (frule_tac c' = c in usableRange_subseteq) + apply (drule (1) aligned_untypedRange_non_empty) + apply assumption + apply (drule (1) aligned_untypedRange_non_empty)+ + apply (drule untypedCapRange)+ + apply (thin_tac "All P" for P) + apply (subgoal_tac "untypedRange cap \ untypedRange c = {}") + apply (intro conjI) + apply simp + apply (drule(2) set_inter_not_emptyD1) + apply fastforce + apply (drule(2) set_inter_not_emptyD2) + apply fastforce + apply (drule(2) set_inter_not_emptyD3) + apply simp+ + apply (rule disjoint_subset2[OF _ disjoint_subset]) + apply (rule untypedRange_in_capRange)+ + apply (simp add:Int_ac) + done +context begin interpretation Arch . (*FIXME: arch_split*) +lemma valid_nullcaps_init: + "\ valid_nullcaps m; cap \ NullCap \ \ valid_nullcaps (m(p \ CTE cap initMDBNode))" + by (simp add: valid_nullcaps_def initMDBNode_def nullPointer_def) +end + +lemma class_links_init: + "\ class_links m; no_0 m; m p = Some cte; + no_mdb cte; valid_dlist m \ + \ class_links (m(p \ CTE cap initMDBNode))" + apply (simp add: class_links_def split del: if_split) + apply (erule allEI, erule allEI) + apply simp + apply (intro conjI impI) + apply clarsimp + apply (drule no_mdb_not_target[where p=p], simp) + apply (simp add: no_mdb_def) + apply (erule(2) valid_dlist_init) + apply (clarsimp simp add: no_0_def) + apply simp + apply (clarsimp simp: mdb_next_unfold) + apply (clarsimp simp: mdb_next_unfold) + done + +lemma distinct_zombies_copyE: + "\ distinct_zombies m; m x = Some cte; + capClass (cteCap cte') = PhysicalClass + \ isZombie (cteCap cte) = isZombie (cteCap cte'); + \ capClass (cteCap cte') = PhysicalClass; isUntypedCap (cteCap cte) \ + \ isUntypedCap (cteCap cte'); + \ capClass (cteCap cte') = PhysicalClass; isArchFrameCap (cteCap cte) \ + \ isArchFrameCap (cteCap cte'); + isZombie (cteCap cte') \ x = y; + capClass (cteCap cte') = PhysicalClass \ + capBits (cteCap cte') = capBits (cteCap cte); + capClass (cteCap cte') = PhysicalClass \ capClass (cteCap cte) = PhysicalClass; + capClass (cteCap cte') = PhysicalClass \ + capUntypedPtr (cteCap cte') = capUntypedPtr (cteCap cte) \ + \ distinct_zombies (m (y \ cte'))" + apply (simp add: distinct_zombies_def distinct_zombie_caps_def) + apply clarsimp + apply (intro allI conjI impI) + apply clarsimp + apply (drule_tac x=y in spec) + apply (drule_tac x=ptr' in spec) + apply (clarsimp simp: isCap_simps) + apply clarsimp + apply (drule_tac x=ptr in spec) + apply (drule_tac x=x in spec) + apply clarsimp + apply auto[1] + apply clarsimp + apply (drule_tac x=ptr in spec) + apply (drule_tac x=ptr' in spec) + apply auto[1] + done + +lemmas distinct_zombies_sameE + = distinct_zombies_copyE [where y=x and x=x for x, simplified, + OF _ _ _ _ _] +context begin interpretation Arch . (*FIXME: arch_split*) +lemma capBits_Master: + "capBits (capMasterCap cap) = capBits cap" + by (clarsimp simp: capMasterCap_def split: capability.split arch_capability.split) + +lemma capUntyped_Master: + "capUntypedPtr (capMasterCap cap) = capUntypedPtr cap" + by (clarsimp simp: capMasterCap_def RISCV64_H.capUntypedPtr_def split: capability.split arch_capability.split) + +lemma distinct_zombies_copyMasterE: + "\ distinct_zombies m; m x = Some cte; + capClass (cteCap cte') = PhysicalClass + \ capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); + isZombie (cteCap cte') \ x = y \ + \ distinct_zombies (m (y \ cte'))" + apply (erule(1) distinct_zombies_copyE, simp_all) + apply (rule master_eqI, rule isCap_Master, simp) + apply (drule_tac f=isUntypedCap in arg_cong) + apply (simp add: isCap_Master) + apply (drule_tac f=isArchFrameCap in arg_cong) + apply (simp add: isCap_Master) + apply (rule master_eqI, rule capBits_Master, simp) + apply clarsimp + apply (drule_tac f=capClass in arg_cong, simp add: capClass_Master) + apply (drule_tac f=capUntypedPtr in arg_cong, simp add: capUntyped_Master) + done + +lemmas distinct_zombies_sameMasterE + = distinct_zombies_copyMasterE[where x=x and y=x for x, simplified, + OF _ _ _] + +lemma isZombie_capClass: "isZombie cap \ capClass cap = PhysicalClass" + by (clarsimp simp: isCap_simps) + +lemma distinct_zombies_unzombieE: + "\ distinct_zombies m; m x = Some cte; + isZombie (cteCap cte') \ isZombie (cteCap cte); + isUntypedCap (cteCap cte) \ isUntypedCap (cteCap cte'); + isArchFrameCap (cteCap cte) \ isArchFrameCap (cteCap cte'); + capClass (cteCap cte') = capClass (cteCap cte); + capBits (cteCap cte') = capBits (cteCap cte); + capUntypedPtr (cteCap cte') = capUntypedPtr (cteCap cte) \ + \ distinct_zombies (m(x \ cte'))" + apply (simp add: distinct_zombies_def distinct_zombie_caps_def + split del: if_split) + apply (erule allEI, erule allEI) + apply clarsimp + done + +lemma distinct_zombies_seperateE: + "\ distinct_zombies m; + \y cte. m y = Some cte \ x \ y + \ \ isUntypedCap (cteCap cte) + \ \ isArchFrameCap (cteCap cte) + \ capClass (cteCap cte) = PhysicalClass + \ capClass (cteCap cte') = PhysicalClass + \ capUntypedPtr (cteCap cte) = capUntypedPtr (cteCap cte') + \ capBits (cteCap cte) = capBits (cteCap cte') \ False \ + \ distinct_zombies (m (x \ cte'))" + apply (simp add: distinct_zombies_def distinct_zombie_caps_def) + apply (intro impI allI conjI) + apply (clarsimp simp: isZombie_capClass) + apply fastforce + apply clarsimp + apply (frule isZombie_capClass) + apply (subgoal_tac "\ isUntypedCap (cteCap z) \ \ isArchFrameCap (cteCap z)") + apply fastforce + apply (clarsimp simp: isCap_simps) + apply clarsimp + apply (erule notE[rotated], elim allE, erule mp) + apply auto[1] + done + +lemma distinct_zombies_init: + "\ distinct_zombies m; caps_no_overlap' m (capRange (cteCap cte)); + capAligned (cteCap cte); \x cte. m x = Some cte \ capAligned (cteCap cte) \ + \ distinct_zombies (m (p \ cte))" + apply (erule distinct_zombies_seperateE) + apply (rename_tac y cte') + apply (clarsimp simp: caps_no_overlap'_def) + apply (drule_tac x=y in spec)+ + apply (case_tac cte') + apply (rename_tac capability mdbnode) + apply clarsimp + apply (subgoal_tac "capRange capability \ capRange (cteCap cte)") + apply (clarsimp simp: capRange_def) + apply (drule(1) capAligned_capUntypedPtr)+ + apply clarsimp + done + +definition + "no_irq' m \ \p cte. m p = Some cte \ cteCap cte \ IRQControlCap" + +lemma no_irqD': + "\ m p = Some (CTE IRQControlCap n); no_irq' m \ \ False" + unfolding no_irq'_def + apply (erule allE, erule allE, erule (1) impE) + apply auto + done + +lemma irq_control_init: + assumes no_irq: "cap = IRQControlCap \ no_irq' m" + assumes ctrl: "irq_control m" + shows "irq_control (m(p \ CTE cap initMDBNode))" + using no_irq + apply (clarsimp simp: irq_control_def) + apply (rule conjI) + apply (clarsimp simp: initMDBNode_def) + apply (erule (1) no_irqD') + apply clarsimp + apply (frule irq_revocable, rule ctrl) + apply clarsimp + apply (rule conjI) + apply clarsimp + apply (erule (1) no_irqD') + apply clarsimp + apply (erule (1) irq_controlD, rule ctrl) + done + +lemma valid_mdb_ctes_init: + "\ valid_mdb_ctes m; m p = Some cte; no_mdb cte; + caps_no_overlap' m (capRange cap); s \' cap; + valid_objs' s; m = ctes_of s; cap \ NullCap; + fresh_virt_cap_class (capClass cap) (ctes_of s); + cap = capability.IRQControlCap \ no_irq' (ctes_of s) \ \ + valid_mdb_ctes (m (p \ CTE cap initMDBNode))" + apply (simp add: valid_mdb_ctes_def) + apply (rule conjI, rule valid_dlist_init, simp+) + apply (subgoal_tac "p \ 0") + prefer 2 + apply (erule no_0_neq, clarsimp) + apply (clarsimp simp: no_0_update) + apply (rule conjI, rule mdb_chain_0_update_0, simp+) + apply (rule conjI, rule valid_badges_0_update, simp+) + apply (rule conjI, erule (1) caps_contained_no_overlap) + apply (rule conjI, rule mdb_chunked_init, simp+) + apply (rule conjI) + apply (rule untyped_mdb_init, (simp add: valid_mdb_ctes_def)+) + apply (rule conjI) + apply (rule untyped_inc_init, (simp add: valid_mdb_ctes_def)+) + apply (rule conjI) + apply (erule(1) valid_nullcaps_init) + apply (rule conjI, simp add: ut_revocable'_def initMDBNode_def) + apply (rule conjI, erule(4) class_links_init) + apply (rule conjI) + apply (erule distinct_zombies_init, simp+) + apply (erule valid_capAligned) + apply clarsimp + apply (case_tac ctea, clarsimp) + apply (rule valid_capAligned, erule(1) ctes_of_valid_cap') + apply (rule conjI) + apply (erule (1) irq_control_init) + apply (simp add: ran_def reply_masters_rvk_fb_def) + apply (auto simp: initMDBNode_def)[1] + done + +lemma setCTE_state_refs_of'[wp]: + "\\s. P (state_refs_of' s)\ setCTE p cte \\rv s. P (state_refs_of' s)\" + unfolding setCTE_def + apply (rule setObject_state_refs_of_eq) + apply (clarsimp simp: updateObject_cte in_monad typeError_def + in_magnitude_check objBits_simps + split: kernel_object.split_asm if_split_asm) + done + +lemma setCTE_valid_mdb: + fixes cap + defines "cte \ CTE cap initMDBNode" + shows + "\\s. valid_mdb' s \ cte_wp_at' no_mdb ptr s \ + s \' cap \ valid_objs' s \ cap \ NullCap \ + caps_no_overlap' (ctes_of s) (capRange cap) \ + fresh_virt_cap_class (capClass cap) (ctes_of s) \ + (cap = capability.IRQControlCap \ no_irq' (ctes_of s))\ + setCTE ptr cte + \\r. valid_mdb'\" + apply (simp add: valid_mdb'_def setCTE_def cte_def cte_wp_at_ctes_of) + apply (wp ctes_of_setObject_cte) + apply (clarsimp simp del: fun_upd_apply) + apply (erule (8) valid_mdb_ctes_init [OF _ _ _ _ _ _ refl]) + done + +lemma setCTE_valid_objs'[wp]: + "\valid_objs' and (valid_cap' (cteCap cte)) \ + setCTE p cte \\rv. valid_objs'\" + unfolding setCTE_def + apply (rule setObject_valid_objs') + apply (clarsimp simp: prod_eq_iff lookupAround2_char1 updateObject_cte objBits_simps) + apply (clarsimp simp: prod_eq_iff lookupAround2_char1 + updateObject_cte in_monad typeError_def + valid_obj'_def valid_tcb'_def valid_cte'_def + tcb_cte_cases_def cteSizeBits_def + split: kernel_object.split_asm if_split_asm) + done + +lemma getCTE_cte_wp_at: + "\\\ getCTE p \\rv. cte_wp_at' (\c. c = rv) p\" + apply (clarsimp simp: valid_def cte_wp_at'_def getCTE_def) + apply (frule state_unchanged [OF getObject_cte_inv]) + apply simp + apply (drule getObject_cte_det, simp) + done + +lemma getCTE_sp: + "\P\ getCTE p \\rv. cte_wp_at' (\c. c = rv) p and P\" + apply (rule hoare_chain) + apply (rule hoare_vcg_conj_lift) + apply (rule getCTE_cte_wp_at) + apply (rule getCTE_inv) + apply (rule conjI, rule TrueI, assumption) + apply simp + done + +lemmas setCTE_ad[wp] = + setObject_aligned[where 'a=cte, folded setCTE_def] + setObject_distinct[where 'a=cte, folded setCTE_def] +lemmas setCTE_map_to_ctes = + ctes_of_setObject_cte[folded setCTE_def] + +lemma getCTE_ctes_wp: + "\\s. \cte. ctes_of s ptr = Some cte \ P cte s\ getCTE ptr \P\" + apply (rule hoare_strengthen_post, rule getCTE_sp) + apply (clarsimp simp: cte_wp_at_ctes_of) + done + +lemma updateMDB_valid_objs'[wp]: + "\valid_objs'\ updateMDB m p \\rv. valid_objs'\" + apply (clarsimp simp add: updateMDB_def) + apply (wp | simp)+ + done + +lemma cte_overwrite: + "cteMDBNode_update (\x. m) (cteCap_update (\x. c) v) = CTE c m" + by (cases v, simp) + +lemma setCTE_no_0_obj' [wp]: + "\no_0_obj'\ setCTE p c \\_. no_0_obj'\" + by (simp add: setCTE_def) wp + +crunch pspace_canonical'[wp]: setCTE "pspace_canonical'" + +crunch pspace_in_kernel_mappings'[wp]: setCTE "pspace_in_kernel_mappings'" + +declare mresults_fail[simp] + +end + +lemma diminished_capMaster: + "diminished' cap cap' \ capMasterCap cap' = capMasterCap cap" + by (clarsimp simp: diminished'_def) + + +end (* of theory *)