(*
 * Copyright 2014, General Dynamics C4 Systems
 *
 * SPDX-License-Identifier: GPL-2.0-only
 *)

(*
   CSpace invariants
*)

theory CSpace_I
imports ArchAcc_R
begin

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 (ARM_H.ASIDPoolCap r asid) = r"
  "Arch.capUntypedPtr (ARM_H.PageCap d r rghts sz mapdata) = r"
  "Arch.capUntypedPtr (ARM_H.PageTableCap r mapdata2) = r"
  "Arch.capUntypedPtr (ARM_H.PageDirectoryCap r mapdata3) = r"
  by (auto simp: capUntypedPtr_def
                 ARM_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
            ARM_H.maskCapRights_def maskVMRights_def
  by (cases c) (simp_all add: Let_def split: arch_capability.split vmrights.split)

lemma getCTE_inv [wp]: "\<lbrace>P\<rbrace> getCTE addr \<lbrace>\<lambda>rv. P\<rbrace>"
  by (simp add: getCTE_def) wp

lemma getEndpoint_inv [wp]:
  "\<lbrace>P\<rbrace> getEndpoint ptr \<lbrace>\<lambda>rv. P\<rbrace>"
  by (simp add: getEndpoint_def getObject_inv loadObject_default_inv)

lemma getNotification_inv [wp]:
  "\<lbrace>P\<rbrace> getNotification ptr \<lbrace>\<lambda>rv. P\<rbrace>"
  by (simp add: getNotification_def getObject_inv loadObject_default_inv)

lemma getSlotCap_inv [wp]: "\<lbrace>P\<rbrace> getSlotCap addr \<lbrace>\<lambda>rv. P\<rbrace>"
  by (simp add: getSlotCap_def, wp)

declare resolveAddressBits.simps[simp del]

lemma cap_case_CNodeCap:
  "(case cap of CNodeCap a b c d \<Rightarrow> P
         | _ \<Rightarrow> Q)
      = (if isCNodeCap cap then P else Q)"
  by (cases cap, simp_all add: isCap_simps)

lemma resolveAddressBits_inv_induct:
  shows
  "s \<turnstile> \<lbrace>P\<rbrace>
     resolveAddressBits cap cref depth
   \<lbrace>\<lambda>rv. P\<rbrace>,\<lbrace>\<lambda>rv. P\<rbrace>"
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]:
  "\<lbrace>P\<rbrace> resolveAddressBits cap addr depth \<lbrace>\<lambda>rv. P\<rbrace>"
  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:
  "\<lbrace>P\<rbrace> updateObject (cte :: cte) ko x y n \<lbrace>\<lambda>rv. P\<rbrace>"
  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 \<equiv> mdbPrev (cteMDBNode cte) = 0 \<and> mdbNext (cteMDBNode cte) = 0"

lemma mdb_next_update:
  "m (x \<mapsto> y) \<turnstile> a \<leadsto> b =
  (if a = x then mdbNext (cteMDBNode y) = b else m \<turnstile> a \<leadsto> b)"
  by (simp add: mdb_next_rel_def mdb_next_def)

lemma neg_no_loopsI:
  "m \<turnstile> c \<leadsto>\<^sup>+ c \<Longrightarrow> \<not> no_loops m"
  unfolding no_loops_def by auto

lemma valid_dlistEp [elim?]:
  "\<lbrakk> valid_dlist m; m p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0;
     \<And>cte'. \<lbrakk> m (mdbPrev (cteMDBNode cte)) = Some cte';
              mdbNext (cteMDBNode cte') = p \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow>
  P"
  unfolding valid_dlist_def Let_def by blast

lemma valid_dlistEn [elim?]:
  "\<lbrakk> valid_dlist m; m p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0;
     \<And>cte'. \<lbrakk> m (mdbNext (cteMDBNode cte)) = Some cte';
              mdbPrev (cteMDBNode cte') = p \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow>
  P"
  unfolding valid_dlist_def Let_def by blast

lemmas valid_dlistE = valid_dlistEn valid_dlistEp

lemma mdb_next_update_other:
  "\<lbrakk> m (x \<mapsto> y) \<turnstile> a \<leadsto> b; x \<noteq> a \<rbrakk> \<Longrightarrow> m \<turnstile> a \<leadsto> b"
  by (simp add: mdb_next_rel_def mdb_next_def)

lemma mdb_trancl_update_other:
  assumes  upd: "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y"
  and   nopath: "\<not> m \<turnstile> x \<leadsto>\<^sup>* p"
  shows "m \<turnstile> x \<leadsto>\<^sup>+ y"
  using upd nopath
proof induct
  case (base y)

  have "m \<turnstile> x \<leadsto> y"
  proof (rule mdb_next_update_other)
    from base show "p \<noteq> x" by clarsimp
  qed fact+

  thus ?case ..
next
  case (step y z)
  hence ih: "m \<turnstile> x \<leadsto>\<^sup>+ y" by auto

  from ih show ?case
  proof
    show "m \<turnstile> y \<leadsto> z"
    proof (rule mdb_next_update_other)
      show "p \<noteq> 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 \<turnstile> c \<leadsto> y = (\<exists>cte. m c = Some cte \<and> 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) \<noteq> ptr"
proof -
  from no_loop have "\<not> m \<turnstile> ptr \<leadsto> 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 \<equiv> \<lambda>cte. mdbNext (cteMDBNode cte)"
  and     "prv \<equiv> \<lambda>cte. mdbPrev (cteMDBNode cte)"
  assumes r1: "\<And>p cte. \<lbrakk> m p = Some cte; prv cte \<noteq> 0 \<rbrakk> \<Longrightarrow> \<exists>cte'. m (prv cte) = Some cte' \<and> nxt cte' = p"
  and     r2: "\<And>p cte. \<lbrakk> m p = Some cte; nxt cte \<noteq> 0 \<rbrakk> \<Longrightarrow> \<exists>cte'. m (nxt cte) = Some cte' \<and> 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 \<turnstile> x \<leadsto>\<^sup>+ y"
  shows   "\<not> m \<turnstile> y \<leadsto>\<^sup>* x"
proof
  assume "m \<turnstile> y \<leadsto>\<^sup>* x"
  hence "m \<turnstile> x \<leadsto>\<^sup>+ x" using nxt
    by simp

  thus False using nl
    unfolding no_loops_def by auto
qed

lemma neg_next_rtrancl_trancl:
  "\<lbrakk> \<not> m \<turnstile> y \<leadsto>\<^sup>* r; m \<turnstile> x \<leadsto> y \<rbrakk> \<Longrightarrow> \<not> m \<turnstile> x \<leadsto>\<^sup>+ r"
  apply (erule contrapos_nn)
  apply (drule tranclD)
  apply (clarsimp simp: next_unfold')
  done

lemma next_trancl_split_tt:
  assumes p1: "m \<turnstile> x \<leadsto>\<^sup>+ y"
  and     p2: "m \<turnstile> x \<leadsto>\<^sup>+ p"
  and     nm: "\<not> m \<turnstile> p \<leadsto>\<^sup>* y"
  shows "m \<turnstile> y \<leadsto>\<^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 \<turnstile> y \<leadsto>\<^sup>* q"
    proof (rule step.hyps)
      have "\<not> m \<turnstile> q \<leadsto>\<^sup>+ y"
        by (rule neg_next_rtrancl_trancl) fact+
      thus "\<not> m \<turnstile> q \<leadsto>\<^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 \<turnstile> x \<leadsto>\<^sup>+ p"
  shows "m (p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ p"
proof -
  from noloop nxt have xp: "x \<noteq> 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 \<mapsto> cte) \<turnstile> y \<leadsto> p" using noloop
      by (auto simp add: mdb_next_update)
    thus ?case ..
  next
    case (step y z)

    from noloop step have xp: "z \<noteq> p"
      by (clarsimp dest!: neg_no_loopsI)

    hence "m (p \<mapsto> cte) \<turnstile> y \<leadsto> z" using step
      by (simp add: mdb_next_update)

    moreover from xp have "m (p \<mapsto> cte) \<turnstile> z \<leadsto>\<^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?]:
  "\<lbrakk>m c = Some cte; no_0 m\<rbrakk> \<Longrightarrow> c \<noteq> 0"
  by (auto simp add: no_0_def)

lemma no_0_update:
  assumes no0: "no_0 m"
  and     pnz: "p \<noteq> 0"
  shows "no_0 (m(p \<mapsto> cte))"
  using no0 pnz unfolding no_0_def by simp

lemma mdb_rtrancl_update_other:
  assumes  upd: "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y"
  and   nopath: "\<not> m \<turnstile> x \<leadsto>\<^sup>* p"
  shows "m \<turnstile> x \<leadsto>\<^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 \<turnstile> x \<leadsto>\<^sup>+ y"
  and      np: "\<not> m \<turnstile> x \<leadsto>\<^sup>* p"
  shows   "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y"
  using upd
proof induct
  case (base q)
  from np have "x \<noteq> p" by clarsimp
  hence"m (p \<mapsto> cte) \<turnstile> x \<leadsto> 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 \<noteq> p"
      by (auto elim!: contrapos_nn)

    thus x: "m(p \<mapsto> cte) \<turnstile> q \<leadsto> r"
      using step by (simp add: mdb_next_update del: fun_upd_apply)
  qed fact+
qed

lemma mdb_rtrancl_other_update:
  assumes upd: "m \<turnstile> x \<leadsto>\<^sup>* y"
  and  nopath: "\<not> m \<turnstile> x \<leadsto>\<^sup>* p"
  shows   "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^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 \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* 0"
  and    np: "\<not> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* p"
  assumes p: "p \<noteq> 0"
  assumes 0: "no_0 m"
  assumes n: "mdb_chain_0 m"
  shows "mdb_chain_0 (m(p \<mapsto> cte))"
   unfolding mdb_chain_0_def
proof rule
  fix x
  assume "x \<in> dom (m(p \<mapsto> cte))"
  hence x: "x = p \<or> x \<in> dom m" by simp

  have cnxt: "m(p \<mapsto> cte) \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* 0"
    by (rule mdb_rtrancl_other_update) fact+

  from x show "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ 0"
  proof
    assume xp: "x = p"
    show ?thesis
    proof (rule rtrancl_into_trancl2 [OF _ cnxt])
      show "m(p \<mapsto> cte) \<turnstile> x \<leadsto> mdbNext (cteMDBNode cte)" using xp
        by (simp add: mdb_next_update)
    qed
  next
    assume x: "x \<in> dom m"

    show ?thesis
    proof (cases "m \<turnstile> x \<leadsto>\<^sup>* p")
      case False
      from n have "m \<turnstile> x \<leadsto>\<^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 \<mapsto> cte) \<turnstile> x \<leadsto>\<^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 \<mapsto> cte) \<turnstile> p \<leadsto> 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 \<noteq> 0"
  assumes 0: "no_0 m"
  assumes n: "mdb_chain_0 m"
  shows "mdb_chain_0 (m(p \<mapsto> 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 \<mapsto> cte))"
proof (unfold valid_badges_def, clarify)
  fix c c' cap cap' n n'
  assume c: "(m(p \<mapsto> cte)) c = Some (CTE cap n)"
  assume c': "(m(p \<mapsto> cte)) c' = Some (CTE cap' n')"
  assume nxt: "m(p \<mapsto> cte) \<turnstile> c \<leadsto> c'"
  assume r: "sameRegionAs cap cap'"

  from p 0 have p0: "p \<noteq> 0" by (clarsimp simp: no_0_def)

  from c' p0 0
  have "c' \<noteq> 0" by (clarsimp simp: no_0_def)
  with nx nxt
  have cp: "c \<noteq> p" by (clarsimp simp add: mdb_next_unfold)
  moreover
  from pv nx nxt p p0 c d m 0
  have "c' \<noteq> 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 \<turnstile> c \<leadsto> c'" by (simp add: mdb_next_unfold)
  ultimately
  show "(isEndpointCap cap \<longrightarrow>
            capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow>
            capEPBadge cap' \<noteq> 0 \<longrightarrow>
            mdbFirstBadged n') \<and>
        (isNotificationCap cap \<longrightarrow>
            capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow>
            capNtfnBadge cap' \<noteq> 0 \<longrightarrow>
            mdbFirstBadged n')"
    using r c c' v by (fastforce simp: valid_badges_def)
qed

definition
  "caps_no_overlap' m S \<equiv>
  \<forall>p c n. m p = Some (CTE c n) \<longrightarrow> capRange c \<inter> S = {}"

definition
  fresh_virt_cap_class :: "capclass \<Rightarrow> cte_heap \<Rightarrow> bool"
where
 "fresh_virt_cap_class C m \<equiv>
    C \<noteq> PhysicalClass \<longrightarrow> C \<notin> (capClass \<circ> cteCap) ` ran m"

lemma fresh_virt_cap_class_Physical[simp]:
  "fresh_virt_cap_class PhysicalClass = \<top>"
  by (rule ext, simp add: fresh_virt_cap_class_def)+

lemma fresh_virt_cap_classD:
  "\<lbrakk> m x = Some cte; fresh_virt_cap_class C m \<rbrakk>
     \<Longrightarrow> C \<noteq> PhysicalClass \<longrightarrow> capClass (cteCap cte) \<noteq> C"
  by (auto simp: fresh_virt_cap_class_def)

lemma capRange_untyped:
  "capRange cap' \<inter> untypedRange cap \<noteq> {} \<Longrightarrow> 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:
  "\<lbrakk> caps_no_overlap' m (capRange cap); caps_contained' m\<rbrakk>
    \<Longrightarrow> caps_contained' (m(p \<mapsto> 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:
  "\<lbrakk> m p = Some cte; no_mdb cte; valid_dlist m; no_0 m \<rbrakk> \<Longrightarrow> \<not> m \<turnstile> x \<leadsto> 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:
  "\<lbrakk> m p = Some cte; no_mdb cte; p \<noteq> x; valid_dlist m; no_0 m \<rbrakk> \<Longrightarrow> \<not> m \<turnstile> x \<leadsto>\<^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 ARM_H.isPhysicalCap_def
         split: capability.split arch_capability.split)

(* FIXME instead of a definition and then a simp rule in the simp set, we should use fun *)
definition
  capMasterCap :: "capability \<Rightarrow> capability"
where
 "capMasterCap cap \<equiv> case cap of
   EndpointCap ref bdg s r g gr \<Rightarrow> EndpointCap ref 0 True True True True
 | NotificationCap ref bdg s r \<Rightarrow> NotificationCap ref 0 True True
 | CNodeCap ref bits gd gs \<Rightarrow> CNodeCap ref bits 0 0
 | ThreadCap ref \<Rightarrow> ThreadCap ref
 | ReplyCap ref master g \<Rightarrow> ReplyCap ref True True
 | UntypedCap d ref n f \<Rightarrow> UntypedCap d ref n 0
 | ArchObjectCap acap \<Rightarrow> ArchObjectCap (case acap of
      PageCap d ref rghts sz mapdata \<Rightarrow>
         PageCap d ref VMReadWrite sz None
    | ASIDPoolCap pool asid \<Rightarrow>
         ASIDPoolCap pool 0
    | PageTableCap ptr data \<Rightarrow>
         PageTableCap ptr None
    | PageDirectoryCap ptr data \<Rightarrow>
         PageDirectoryCap ptr None
    | _ \<Rightarrow> acap)
 | _ \<Rightarrow> cap"

lemma capMasterCap_simps[simp]:
  "capMasterCap (EndpointCap ref bdg s r g gr) = EndpointCap ref 0 True True True True"
  "capMasterCap (NotificationCap ref bdg s r) = NotificationCap ref 0 True True"
  "capMasterCap (CNodeCap ref bits gd gs) = CNodeCap ref bits 0 0"
  "capMasterCap (ThreadCap ref) = ThreadCap ref"
  "capMasterCap capability.NullCap = capability.NullCap"
  "capMasterCap capability.DomainCap = capability.DomainCap"
  "capMasterCap (capability.IRQHandlerCap irq) = capability.IRQHandlerCap irq"
  "capMasterCap (capability.Zombie word zombie_type n) = capability.Zombie word zombie_type n"
  "capMasterCap (capability.ArchObjectCap (arch_capability.ASIDPoolCap word1 word2)) =
            capability.ArchObjectCap (arch_capability.ASIDPoolCap word1 0)"
  "capMasterCap (capability.ArchObjectCap arch_capability.ASIDControlCap) =
         capability.ArchObjectCap arch_capability.ASIDControlCap"
  "capMasterCap (capability.ArchObjectCap (arch_capability.PageCap d word vmrights vmpage_size pdata)) =
            capability.ArchObjectCap (arch_capability.PageCap d word VMReadWrite vmpage_size None)"
  "capMasterCap (capability.ArchObjectCap (arch_capability.PageTableCap word ptdata)) =
            capability.ArchObjectCap (arch_capability.PageTableCap word None)"
  "capMasterCap (capability.ArchObjectCap (arch_capability.PageDirectoryCap word pddata)) =
            capability.ArchObjectCap (arch_capability.PageDirectoryCap word None)"
  "capMasterCap (capability.UntypedCap d word n f) = capability.UntypedCap d word n 0"
  "capMasterCap capability.IRQControlCap = capability.IRQControlCap"
  "capMasterCap (capability.ReplyCap word m g) = capability.ReplyCap word True True"
  by (simp_all add: capMasterCap_def)

lemma capMasterCap_eqDs1:
  "capMasterCap cap = EndpointCap ref bdg s r g gr
     \<Longrightarrow> bdg = 0 \<and> s \<and> r \<and> g \<and> gr
          \<and> (\<exists>bdg s r g gr. cap = EndpointCap ref bdg s r g gr)"
  "capMasterCap cap = NotificationCap ref bdg s r
     \<Longrightarrow> bdg = 0 \<and> s \<and> r
          \<and> (\<exists>bdg s r. cap = NotificationCap ref bdg s r)"
  "capMasterCap cap = CNodeCap ref bits gd gs
     \<Longrightarrow> gd = 0 \<and> gs = 0 \<and> (\<exists>gd gs. cap = CNodeCap ref bits gd gs)"
  "capMasterCap cap = ThreadCap ref
     \<Longrightarrow> cap = ThreadCap ref"
  "capMasterCap cap = NullCap
     \<Longrightarrow> cap = NullCap"
  "capMasterCap cap = DomainCap
     \<Longrightarrow> cap = DomainCap"
  "capMasterCap cap = IRQControlCap
     \<Longrightarrow> cap = IRQControlCap"
  "capMasterCap cap = IRQHandlerCap irq
     \<Longrightarrow> cap = IRQHandlerCap irq"
  "capMasterCap cap = Zombie ref tp n
     \<Longrightarrow> cap = Zombie ref tp n"
  "capMasterCap cap = UntypedCap d ref bits 0
     \<Longrightarrow> \<exists>f. cap = UntypedCap d ref bits f"
  "capMasterCap cap = ReplyCap ref master g
     \<Longrightarrow> master \<and> g \<and> (\<exists>master g. cap = ReplyCap ref master g)"
  "capMasterCap cap = ArchObjectCap (PageCap d ref rghts sz mapdata)
     \<Longrightarrow> rghts = VMReadWrite \<and> mapdata = None
          \<and> (\<exists>rghts mapdata. cap = ArchObjectCap (PageCap d ref rghts sz mapdata))"
  "capMasterCap cap = ArchObjectCap ASIDControlCap
     \<Longrightarrow> cap = ArchObjectCap ASIDControlCap"
  "capMasterCap cap = ArchObjectCap (ASIDPoolCap pool asid)
     \<Longrightarrow> asid = 0 \<and> (\<exists>asid. cap = ArchObjectCap (ASIDPoolCap pool asid))"
  "capMasterCap cap = ArchObjectCap (PageTableCap ptr data)
     \<Longrightarrow> data = None \<and> (\<exists>data. cap = ArchObjectCap (PageTableCap ptr data))"
  "capMasterCap cap = ArchObjectCap (PageDirectoryCap ptr data2)
     \<Longrightarrow> data2 = None \<and> (\<exists>data2. cap = ArchObjectCap (PageDirectoryCap ptr data2))"
  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 \<Rightarrow> word32 option"
where
 "capBadge cap \<equiv> 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:
  "\<lbrakk> \<And>cap. F (capMasterCap cap) = F cap; F (capMasterCap cap) = F (capMasterCap cap') \<rbrakk>
     \<Longrightarrow> F cap = F cap'"
  by simp

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"
  "isArchPageCap (capMasterCap cap) = isArchPageCap cap"
  by (simp add: isCap_simps capMasterCap_def
         split: capability.split arch_capability.split)+

lemma capUntypedSize_capBits:
  "capClass cap = PhysicalClass \<Longrightarrow> capUntypedSize cap = 2 ^ (capBits cap)"
  apply (simp add: capUntypedSize_def objBits_simps
                   ARM_H.capUntypedSize_def
                   pteBits_def pdeBits_def
                   ptBits_def pdBits_def
                   shiftl_eq_mult
            split: capability.splits arch_capability.splits
                   zombie_type.splits)
  apply fastforce
  done

lemma sameRegionAs_def2:
 "sameRegionAs cap cap' = (\<lambda>cap cap'.
     (cap = cap'
          \<and> (\<not> isNullCap cap \<and> \<not> isZombie cap
              \<and> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap)
          \<and> (\<not> isNullCap cap' \<and> \<not> isZombie cap'
              \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap'))
      \<or> (capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap
                 \<and> (isUntypedCap cap \<or> (isArchPageCap cap \<and> isArchPageCap cap')))
      \<or> (isIRQControlCap cap \<and> 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 add: range_subset_eq2)
  apply (simp cong: conj_cong)
  apply (simp     add: capMasterCap_def sameRegionAs_def isArchPageCap_def
                split: capability.split
            split del: if_split cong: if_cong)
  apply (simp    add: ARM_H.sameRegionAs_def isCap_simps
               split: arch_capability.split
           split del: if_split cong: if_cong)
  apply (clarsimp simp: capRange_def Let_def)
  apply (simp add: range_subset_eq2 cong: conj_cong)
  by (simp add: conj_comms)

lemma sameObjectAs_def2:
 "sameObjectAs cap cap' = (\<lambda>cap cap'.
     (cap = cap'
          \<and> (\<not> isNullCap cap \<and> \<not> isZombie cap
              \<and> \<not> isUntypedCap cap)
          \<and> (\<not> isNullCap cap' \<and> \<not> isZombie cap'
              \<and> \<not> isUntypedCap cap')
          \<and> (isArchPageCap cap \<longrightarrow> capRange cap \<noteq> {})
          \<and> (isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {})))
           (capMasterCap cap) (capMasterCap cap')"
  apply (simp add: sameObjectAs_def sameRegionAs_def2
                   isCap_simps capMasterCap_def
            split: capability.split)
  apply (clarsimp simp: ARM_H.sameObjectAs_def isCap_simps
                 split: arch_capability.split cong: if_cong)
  apply (clarsimp simp: ARM_H.sameRegionAs_def isCap_simps
             split del: if_split cong: if_cong)
  apply (simp add: capRange_def)
  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:
  "\<lbrakk> sameRegionAs cap cap';
     \<lbrakk> capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap;
         \<not> isUntypedCap cap; \<not> isArchPageCap cap \<rbrakk> \<Longrightarrow> R;
     \<lbrakk> capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap \<rbrakk> \<Longrightarrow> R;
     \<lbrakk> capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap;
          isArchPageCap cap' \<rbrakk> \<Longrightarrow> R;
     \<lbrakk> isIRQControlCap cap; isIRQHandlerCap cap' \<rbrakk> \<Longrightarrow> R
      \<rbrakk> \<Longrightarrow> R"
  by (simp add: sameRegionAs_def3, fastforce)

lemma sameObjectAsE:
  "\<lbrakk> sameObjectAs cap cap';
     \<lbrakk> capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap;
         \<not> isUntypedCap cap;
         isArchPageCap cap \<Longrightarrow> capRange cap \<noteq> {} \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
  by (clarsimp simp add: sameObjectAs_def3)

lemma sameObjectAs_sameRegionAs:
  "sameObjectAs cap cap' \<Longrightarrow> sameRegionAs cap cap'"
  by (clarsimp simp add: sameObjectAs_def2 sameRegionAs_def2)

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 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:
  "\<lbrakk> sameRegionAs cap cap' \<rbrakk> \<Longrightarrow> 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)
   apply (clarsimp simp: isCap_simps)
  done

lemma capAligned_capUntypedPtr:
  "\<lbrakk> capAligned cap; capClass cap = PhysicalClass \<rbrakk> \<Longrightarrow>
   capUntypedPtr cap \<in> capRange cap"
  by (simp add: capRange_def capAligned_def is_aligned_no_overflow)

lemma sameRegionAs_capRange_Int:
  "\<lbrakk> sameRegionAs cap cap'; capClass cap = PhysicalClass \<or> capClass cap' = PhysicalClass;
     capAligned cap; capAligned cap' \<rbrakk>
     \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {}"
  apply (frule sameRegionAs_classes, simp)
  apply (drule(1) capAligned_capUntypedPtr)+
  apply (erule sameRegionAsE)
      apply (subgoal_tac "capRange (capMasterCap cap') \<inter> capRange (capMasterCap cap) \<noteq> {}")
       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:
  "\<lbrakk> sameRegionAs a b; sameRegionAs b c \<rbrakk> \<Longrightarrow> sameRegionAs a c"
  apply (simp add: sameRegionAs_def2, elim conjE disjE, simp_all)
         apply (auto simp: isCap_simps)
    apply (auto simp: capRange_def)
  done

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: ARM_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: ARM_H.maskCapRights_def Let_def isCap_simps)
  done

lemma getObject_cte_det:
  "(r::cte,s') \<in> fst (getObject p s) \<Longrightarrow> fst (getObject p s) = {(r,s)} \<and> 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 \<or> (\<exists>n \<in> dom tcb_cte_cases. obj_at' (P \<circ> (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 projectKOs
           | rule rev_bexI, erule domI)+
  apply fastforce
  done

lemma cte_wp_at_valid_objs_valid_cap':
  "\<lbrakk> cte_wp_at' P p s; valid_objs' s \<rbrakk> \<Longrightarrow> \<exists>cte. P cte \<and> s \<turnstile>' (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: projectKOs valid_obj'_def valid_cte'_def)
  apply (drule(1) obj_at_valid_objs')
  apply (clarsimp simp: projectKOs valid_obj'_def valid_cte'_def valid_tcb'_def)
  apply (fastforce dest: bspec [OF _ ranI])
  done

lemma getCTE_valid_cap:
  "\<lbrace>valid_objs'\<rbrace> getCTE t \<lbrace>\<lambda>cte s. s \<turnstile>' (cteCap cte) \<and> cte_at' t s\<rbrace>"
  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':
  "\<lbrakk> ctes_of s p = Some (CTE c n); valid_objs' s\<rbrakk> \<Longrightarrow> s \<turnstile>' 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 \<Longrightarrow> capAligned c"
  by (simp add: valid_cap'_def)

lemma caps_no_overlap'_no_region:
  "\<lbrakk> caps_no_overlap' m (capRange cap); valid_objs' s;
    m = ctes_of s; s \<turnstile>' cap; fresh_virt_cap_class (capClass cap) m \<rbrakk> \<Longrightarrow>
  \<forall>c n p. m p = Some (CTE c n) \<longrightarrow>
         \<not> sameRegionAs c cap \<and> \<not> 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 \<equiv> 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 \<turnstile>' cap"
  shows "mdb_chunked (m(x \<mapsto> CTE cap initMDBNode))"
  unfolding mdb_chunked_def
proof clarify
  fix p p' c c' n n'
  define m' where "m' \<equiv> m (x \<mapsto> 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 \<noteq> 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 \<noteq> 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 \<noteq> x"
    by (clarsimp simp: m'_def) blast
  moreover
  from p p' r neq no_region
  have p'x: "p' \<noteq> x"
    by (clarsimp simp: m'_def) blast
  ultimately
  have m:
   "(m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and>
    (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m c p p') \<and>
    (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> 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: "\<not> m \<turnstile> p \<leadsto>\<^sup>* x" by (rule no_mdb_rtrancl)

  from x no_m p'x [symmetric] dlist no_0
  have np'x: "\<not> m \<turnstile> p' \<leadsto>\<^sup>* x" by (rule no_mdb_rtrancl)

  show "(m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and>
        (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' c p p') \<and>
        (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p)"
  proof (cases "m \<turnstile> p \<leadsto>\<^sup>+ p'")
    case True
    with m
    have ch: "is_chunk m c p p'" by simp

    from True npx
    have "m' \<turnstile> p \<leadsto>\<^sup>+ p'"
      unfolding m'_def
      by (rule mdb_trancl_other_update)
    moreover
    with nl
    have "\<not> m' \<turnstile> p' \<leadsto>\<^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' \<turnstile> p \<leadsto>\<^sup>+ p''"
      with npx
      have "m \<turnstile> p \<leadsto>\<^sup>+ p''"
        unfolding m'_def
        by - (rule mdb_trancl_update_other)
      moreover
      then
      have p''x: "p'' \<noteq> 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' \<turnstile> p'' \<leadsto>\<^sup>* p'"
      {
        moreover
        from x no_m p''x [symmetric] dlist no_0
        have "\<not>m \<turnstile> p'' \<leadsto>\<^sup>* x" by (rule no_mdb_rtrancl)
        ultimately
        have "m \<turnstile> p'' \<leadsto>\<^sup>* p'"
          unfolding m'_def
          by (rule mdb_rtrancl_update_other)
      }
      ultimately
      have "\<exists>cap'' n''.
            m p'' = Some (CTE cap'' n'') \<and> sameRegionAs c cap''"
        using ch
        by (simp add: is_chunk_def)
      with p''x
      show "\<exists>cap'' n''.
             m' p'' = Some (CTE cap'' n'') \<and> sameRegionAs c cap''"
        by (simp add: m'_def)
    qed
    ultimately
    show ?thesis by simp
  next
    case False
    with m
    have p'p: "m \<turnstile> p' \<leadsto>\<^sup>+ p" by simp
    with m
    have ch: "is_chunk m c' p' p" by simp
    from p'p np'x
    have "m' \<turnstile> p' \<leadsto>\<^sup>+ p"
      unfolding m'_def
      by (rule mdb_trancl_other_update)
    moreover
    with nl
    have "\<not> m' \<turnstile> p \<leadsto>\<^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' \<turnstile> p' \<leadsto>\<^sup>+ p''"
      with np'x
      have "m \<turnstile> p' \<leadsto>\<^sup>+ p''"
        unfolding m'_def
        by - (rule mdb_trancl_update_other)
      moreover
      then
      have p''x: "p'' \<noteq> 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' \<turnstile> p'' \<leadsto>\<^sup>* p"
      {
        moreover
        from x no_m p''x [symmetric] dlist no_0
        have "\<not>m \<turnstile> p'' \<leadsto>\<^sup>* x" by (rule no_mdb_rtrancl)
        ultimately
        have "m \<turnstile> p'' \<leadsto>\<^sup>* p"
          unfolding m'_def
          by (rule mdb_rtrancl_update_other)
      }
      ultimately
      have "\<exists>cap'' n''.
            m p'' = Some (CTE cap'' n'') \<and> sameRegionAs c' cap''"
        using ch
        by (simp add: is_chunk_def)
      with p''x
      show "\<exists>cap'' n''.
             m' p'' = Some (CTE cap'' n'') \<and> sameRegionAs c' cap''"
        by (simp add: m'_def)
    qed
    ultimately
    show ?thesis by simp
  qed
qed

lemma cte_refs_capRange:
  "\<lbrakk> s \<turnstile>' c; \<forall>irq. c \<noteq> IRQHandlerCap irq \<rbrakk> \<Longrightarrow> cte_refs' c x \<subseteq> 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 word_le_minus_one_leq, simp)
    apply (erule is_aligned_no_wrap'[where off="2^tcbBlockSizeBits - 1", simplified field_simps])
    apply (drule word_le_minus_one_leq)
    apply simp
   defer
   \<comment> \<open>CNodeCap\<close>
   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 (erule(1) is_aligned_no_wrap')
    apply (simp add: add_diff_eq[symmetric])
    apply (rule word_plus_mono_right)
     apply simp
    apply (erule is_aligned_no_wrap')
    apply simp
   apply (simp add: power_add field_simps)
   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)
  \<comment> \<open>Zombie\<close>
  apply (clarsimp simp: capAligned_def valid_cap'_def objBits_simps)
  apply (rename_tac word zombie_type nat x)
  apply (subgoal_tac "x * 2^cteSizeBits < 2 ^ zBits zombie_type")
   apply (intro conjI)
    apply (erule(1) is_aligned_no_wrap')
   apply (simp add: add_diff_eq[symmetric])
   apply (rule word_plus_mono_right)
    apply simp
   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 \<Longrightarrow> capRange cap = untypedRange cap"
  by (clarsimp simp: isCap_simps)

lemma no_direct_loop [simp]:
  "no_loops m \<Longrightarrow> m (mdbNext node) \<noteq> 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 \<Longrightarrow> m \<turnstile> x \<leadsto> x = False"
  by (auto simp add: no_loops_def)

lemma no_loops_trancl_simp:
  "no_loops m \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ x = False"
  by (auto simp add: no_loops_def)

lemma subtree_mdb_next:
  "m \<turnstile> a \<rightarrow> b \<Longrightarrow> m \<turnstile> a \<leadsto>\<^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 \<turnstile> x \<leadsto> x = False"
  using no_loops by (rule no_loops_direct_simp)

lemma irrefl_trancl_simp [iff]:
  "m \<turnstile> x \<leadsto>\<^sup>+ x = False"
  using no_loops by (rule no_loops_trancl_simp)

lemma irrefl_subtree [iff]:
  "m \<turnstile> x \<rightarrow> 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 \<and> mdbNext src_node = 0)"
proof -
  { assume "mdbPrev src_node = mdbNext src_node"
    moreover
    assume "mdbNext src_node \<noteq> 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 \<turnstile> src \<leadsto>\<^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 \<and> 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 \<and> 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 \<and> 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]:
  "\<not>m \<turnstile> p \<rightarrow> 0"
  apply clarsimp
  apply (erule subtree.cases)
  apply auto
  done

lemma not_0_subtree [simp]:
  "\<not>m \<turnstile> 0 \<rightarrow> p"
  apply clarsimp
  apply (erule subtree.induct)
  apply (auto simp: mdb_next_unfold)
  done

lemma not_0_next [simp]:
  "\<not> m \<turnstile> 0 \<leadsto> p"
  by (clarsimp simp: mdb_next_unfold)

lemma not_0_trancl [simp]:
  "\<not> m \<turnstile> 0 \<leadsto>\<^sup>+ p"
  by (clarsimp dest!: tranclD)

lemma rtrancl0 [simp]:
  "m \<turnstile> 0 \<leadsto>\<^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) \<noteq> 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) \<noteq> ptr"
proof
  assume prev: "mdbPrev (cteMDBNode cte) = ptr"

  from vmdb have "no_0 m" ..
  with lup have "ptr \<noteq> 0"
    by (rule no_0_neq)

  moreover have "mdbNext (cteMDBNode cte) \<noteq> 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 \<noteq> 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' \<or> mdbNext node = 0 \<and> 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' \<noteq> 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' \<or> mdbNext node = 0 \<and> 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' \<or> mdbPrev node = 0 \<and> 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' \<noteq> 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' \<or> mdbPrev node = 0 \<and> 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 \<turnstile> mdbPrev node \<leftarrow> p"
  using m_p by (clarsimp simp: mdb_prev_def)

lemma m_p_next [intro!]:
  "m \<turnstile> p \<leadsto> mdbNext node"
  using m_p by (clarsimp simp: mdb_next_unfold)

lemma next_p_prev:
  "mdbNext node \<noteq> 0 \<Longrightarrow> m \<turnstile> p \<leftarrow> mdbNext node"
  by (rule dlist_nextD0 [OF m_p_next])

lemma prev_p_next:
  "mdbPrev node \<noteq> 0 \<Longrightarrow> m \<turnstile> mdbPrev node \<leadsto> p"
  by (rule dlist_prevD0 [OF m_p_prev])

lemma p_next:
  "(m \<turnstile> p \<leadsto> p') = (p' = mdbNext node)"
  using m_p by (auto simp: mdb_next_unfold)

end (* of locale mdb_ptr *)

lemma no_mdb_not_target:
  "\<lbrakk> m \<turnstile> c \<leadsto> c'; m p = Some cte; no_mdb cte; valid_dlist m; no_0 m \<rbrakk>
  \<Longrightarrow> c' \<noteq> p"
  apply clarsimp
  apply (subgoal_tac "c \<noteq> 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:
  "\<lbrakk> valid_dlist m; m p = Some cte; no_mdb cte \<rbrakk> \<Longrightarrow>
  valid_dlist (m (p \<mapsto> 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 \<mapsto> 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' \<noteq> 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'\<noteq>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'\<noteq>p")
   prefer 2
   apply (insert n)[1]
   apply (clarsimp simp: mdb_next_unfold m_p no_mdb_def)
  apply (subgoal_tac "p'\<noteq>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:
  "\<lbrakk> valid_mdb_ctes m; m p = Some cte; no_mdb cte;
     caps_no_overlap' m (capRange cap); untyped_mdb' m;
     valid_objs' s; s \<turnstile>' cap;
     m = ctes_of s\<rbrakk>
    \<Longrightarrow> untyped_mdb' (m(p \<mapsto> 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:
  "\<lbrakk>capAligned c; isUntypedCap c\<rbrakk> \<Longrightarrow> untypedRange c \<noteq> {}"
  apply (frule untypedCapRange)
  apply (drule capAligned_capUntypedPtr)
   apply (clarsimp simp: isCap_simps)
  apply blast
  done

lemma untypedRange_not_emptyD: "untypedRange c' \<noteq> {} \<Longrightarrow> isUntypedCap c'"
  by (case_tac c'; simp add: isCap_simps)

lemma usableRange_subseteq:
  "\<lbrakk>capAligned c';isUntypedCap c'\<rbrakk> \<Longrightarrow> usableUntypedRange c' \<subseteq> untypedRange c'"
  apply (clarsimp simp:isCap_simps capAligned_def 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 \<subseteq> capRange x"
  by (case_tac x; simp add: capRange_def)

lemma untyped_inc_init:
  "\<lbrakk> valid_mdb_ctes m; m p = Some cte; no_mdb cte;
     caps_no_overlap' m (capRange cap);
     valid_objs' s; s \<turnstile>' cap;
     m = ctes_of s\<rbrakk>
    \<Longrightarrow> untyped_inc' (m(p \<mapsto> 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 \<inter> 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 \<inter> 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:
  "\<lbrakk> valid_nullcaps m; cap \<noteq> NullCap \<rbrakk> \<Longrightarrow> valid_nullcaps (m(p \<mapsto> CTE cap initMDBNode))"
  by (simp add: valid_nullcaps_def initMDBNode_def nullPointer_def)
end

lemma class_links_init:
  "\<lbrakk> class_links m; no_0 m; m p = Some cte;
     no_mdb cte; valid_dlist m \<rbrakk>
   \<Longrightarrow> class_links (m(p \<mapsto> 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:
  "\<lbrakk> distinct_zombies m; m x = Some cte;
       capClass (cteCap cte') = PhysicalClass
               \<Longrightarrow> isZombie (cteCap cte) = isZombie (cteCap cte');
       \<lbrakk> capClass (cteCap cte') = PhysicalClass; isUntypedCap (cteCap cte) \<rbrakk>
               \<Longrightarrow> isUntypedCap (cteCap cte');
       \<lbrakk> capClass (cteCap cte') = PhysicalClass; isArchPageCap (cteCap cte) \<rbrakk>
               \<Longrightarrow> isArchPageCap (cteCap cte');
       isZombie (cteCap cte') \<Longrightarrow> x = y;
       capClass (cteCap cte') = PhysicalClass \<Longrightarrow>
               capBits (cteCap cte') = capBits (cteCap cte);
       capClass (cteCap cte') = PhysicalClass \<longrightarrow> capClass (cteCap cte) = PhysicalClass;
       capClass (cteCap cte') = PhysicalClass \<Longrightarrow>
            capUntypedPtr (cteCap cte') = capUntypedPtr (cteCap cte) \<rbrakk>
        \<Longrightarrow> distinct_zombies (m (y \<mapsto> 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 split: capability.split arch_capability.split)

lemma distinct_zombies_copyMasterE:
  "\<lbrakk> distinct_zombies m; m x = Some cte;
          capClass (cteCap cte') = PhysicalClass
             \<Longrightarrow> capMasterCap (cteCap cte) = capMasterCap (cteCap cte');
          isZombie (cteCap cte') \<Longrightarrow> x = y \<rbrakk>
       \<Longrightarrow> distinct_zombies (m (y \<mapsto> 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=isArchPageCap 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 \<Longrightarrow> capClass cap = PhysicalClass"
  by (clarsimp simp: isCap_simps)

lemma distinct_zombies_unzombieE:
  "\<lbrakk> distinct_zombies m; m x = Some cte;
        isZombie (cteCap cte') \<longrightarrow> isZombie (cteCap cte);
        isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte');
        isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte');
        capClass (cteCap cte') = capClass (cteCap cte);
        capBits (cteCap cte') = capBits (cteCap cte);
        capUntypedPtr (cteCap cte') = capUntypedPtr (cteCap cte) \<rbrakk>
          \<Longrightarrow> distinct_zombies (m(x \<mapsto> 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:
  "\<lbrakk> distinct_zombies m;
      \<And>y cte. m y = Some cte \<Longrightarrow> x \<noteq> y
                \<Longrightarrow> \<not> isUntypedCap (cteCap cte)
                \<Longrightarrow> \<not> isArchPageCap (cteCap cte)
                \<Longrightarrow> capClass (cteCap cte) = PhysicalClass
                \<Longrightarrow> capClass (cteCap cte') = PhysicalClass
                \<Longrightarrow> capUntypedPtr (cteCap cte) = capUntypedPtr (cteCap cte')
                \<Longrightarrow> capBits (cteCap cte) = capBits (cteCap cte') \<Longrightarrow> False \<rbrakk>
       \<Longrightarrow> distinct_zombies (m (x \<mapsto> 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 "\<not> isUntypedCap (cteCap z) \<and> \<not> isArchPageCap (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:
  "\<lbrakk> distinct_zombies m; caps_no_overlap' m (capRange (cteCap cte));
        capAligned (cteCap cte); \<forall>x cte. m x = Some cte \<longrightarrow> capAligned (cteCap cte) \<rbrakk>
       \<Longrightarrow> distinct_zombies (m (p \<mapsto> 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 \<noteq> capRange (cteCap cte)")
   apply (clarsimp simp: capRange_def)
  apply (drule(1) capAligned_capUntypedPtr)+
  apply clarsimp
  done

definition
  "no_irq' m \<equiv> \<forall>p cte. m p = Some cte \<longrightarrow> cteCap cte \<noteq> IRQControlCap"

lemma no_irqD':
  "\<lbrakk> m p = Some (CTE IRQControlCap n); no_irq' m \<rbrakk> \<Longrightarrow> 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 \<longrightarrow> no_irq' m"
  assumes ctrl: "irq_control m"
  shows "irq_control (m(p \<mapsto> 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:
  "\<lbrakk> valid_mdb_ctes m; m p = Some cte; no_mdb cte;
     caps_no_overlap' m (capRange cap); s \<turnstile>' cap;
     valid_objs' s; m = ctes_of s; cap \<noteq> NullCap;
     fresh_virt_cap_class (capClass cap) (ctes_of s);
     cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s) \<rbrakk> \<Longrightarrow>
  valid_mdb_ctes (m (p \<mapsto> CTE cap initMDBNode))"
  apply (simp add: valid_mdb_ctes_def)
  apply (rule conjI, rule valid_dlist_init, simp+)
  apply (subgoal_tac "p \<noteq> 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]:
  "\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>"
  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 \<equiv> CTE cap initMDBNode"
  shows
  "\<lbrace>\<lambda>s. valid_mdb' s \<and> cte_wp_at' no_mdb ptr s \<and>
        s \<turnstile>' cap \<and> valid_objs' s \<and> cap \<noteq> NullCap \<and>
        caps_no_overlap' (ctes_of s) (capRange cap) \<and>
        fresh_virt_cap_class (capClass cap) (ctes_of s) \<and>
        (cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s))\<rbrace>
  setCTE ptr cte
  \<lbrace>\<lambda>r. valid_mdb'\<rbrace>"
  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]:
  "\<lbrace>valid_objs' and (valid_cap' (cteCap cte)) \<rbrace>
    setCTE p cte \<lbrace>\<lambda>rv. valid_objs'\<rbrace>"
  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
                  split: kernel_object.split_asm if_split_asm)
  done

lemma getCTE_cte_wp_at:
  "\<lbrace>\<top>\<rbrace> getCTE p \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. c = rv) p\<rbrace>"
  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:
  "\<lbrace>P\<rbrace> getCTE p \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. c = rv) p and P\<rbrace>"
  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:
  "\<lbrace>\<lambda>s. \<forall>cte. ctes_of s ptr = Some cte \<longrightarrow> P cte s\<rbrace> getCTE ptr \<lbrace>P\<rbrace>"
  apply (rule hoare_strengthen_post, rule getCTE_sp)
  apply (clarsimp simp: cte_wp_at_ctes_of)
  done

lemma updateMDB_valid_objs'[wp]:
  "\<lbrace>valid_objs'\<rbrace> updateMDB m p \<lbrace>\<lambda>rv. valid_objs'\<rbrace>"
  apply (clarsimp simp add: updateMDB_def)
  apply (wp | simp)+
  done

lemma cte_overwrite:
  "cteMDBNode_update (\<lambda>x. m) (cteCap_update (\<lambda>x. c) v) = CTE c m"
  by (cases v, simp)

lemma setCTE_no_0_obj' [wp]:
  "\<lbrace>no_0_obj'\<rbrace> setCTE p c \<lbrace>\<lambda>_. no_0_obj'\<rbrace>"
  by (simp add: setCTE_def) wp

declare mresults_fail[simp]

crunch idle[wp]: get_object "valid_idle"
  (wp: crunch_wps simp: crunch_simps)

end


end (* of theory *)