kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace1_R

lemma updateMDB_no_0 [wp]:
  "\<lbrace>\<lambda>s. no_0 (ctes_of s)\<rbrace>
  updateMDB p f
  \<lbrace>\<lambda>rv s. no_0 (ctes_of s)\<rbrace>" by wp simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_0 (ctes_of s)\<rbrace> updateMDB p f \<lbrace>\<lambda>rv s. no_0 (ctes_of s)\<rbrace>
theory CSpace1_R

lemma isMDBParentOf_next_update [simp]:
  "isMDBParentOf (cteMDBNode_update (mdbNext_update f) cte) cte' =
   isMDBParentOf cte cte'"
  "isMDBParentOf cte (cteMDBNode_update (mdbNext_update f) cte') =
   isMDBParentOf cte cte'" apply (cases cte) apply (cases cte') apply (simp add: isMDBParentOf_def) apply (cases cte) apply (cases cte') apply (clarsimp simp: isMDBParentOf_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isMDBParentOf (cteMDBNode_update (mdbNext_update f) cte) cte' = isMDBParentOf cte cte' &&& isMDBParentOf cte (cteMDBNode_update (mdbNext_update f) cte') = isMDBParentOf cte cte' proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. cte = CTE x1 x2 \<Longrightarrow> isMDBParentOf (cteMDBNode_update (mdbNext_update f) cte) cte' = isMDBParentOf cte cte'
 2. isMDBParentOf cte (cteMDBNode_update (mdbNext_update f) cte') = isMDBParentOf cte cte' proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>cte = CTE x1 x2; cte' = CTE x1a x2a\<rbrakk> \<Longrightarrow> isMDBParentOf (cteMDBNode_update (mdbNext_update f) cte) cte' = isMDBParentOf cte cte'
 2. isMDBParentOf cte (cteMDBNode_update (mdbNext_update f) cte') = isMDBParentOf cte cte' proof (prove)
goal (1 subgoal):
 1. isMDBParentOf cte (cteMDBNode_update (mdbNext_update f) cte') = isMDBParentOf cte cte' proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. cte = CTE x1 x2 \<Longrightarrow> isMDBParentOf cte (cteMDBNode_update (mdbNext_update f) cte') = isMDBParentOf cte cte' proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>cte = CTE x1 x2; cte' = CTE x1a x2a\<rbrakk> \<Longrightarrow> isMDBParentOf cte (cteMDBNode_update (mdbNext_update f) cte') = isMDBParentOf cte cte' proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma isMDBParentOf_next_update_cte [simp]:
  "isMDBParentOf (CTE cap (mdbNext_update f node)) cte' =
   isMDBParentOf (CTE cap node) cte'"
  "isMDBParentOf cte (CTE cap (mdbNext_update f node)) =
   isMDBParentOf cte (CTE cap node)" apply (cases cte') apply (simp add: isMDBParentOf_def) apply (cases cte) apply (clarsimp simp: isMDBParentOf_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isMDBParentOf (CTE cap (mdbNext_update f node)) cte' = isMDBParentOf (CTE cap node) cte' &&& isMDBParentOf cte (CTE cap (mdbNext_update f node)) = isMDBParentOf cte (CTE cap node) proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. cte' = CTE x1 x2 \<Longrightarrow> isMDBParentOf (CTE cap (mdbNext_update f node)) cte' = isMDBParentOf (CTE cap node) cte'
 2. isMDBParentOf cte (CTE cap (mdbNext_update f node)) = isMDBParentOf cte (CTE cap node) proof (prove)
goal (1 subgoal):
 1. isMDBParentOf cte (CTE cap (mdbNext_update f node)) = isMDBParentOf cte (CTE cap node) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. cte = CTE x1 x2 \<Longrightarrow> isMDBParentOf cte (CTE cap (mdbNext_update f node)) = isMDBParentOf cte (CTE cap node) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma valid_mdbD1':
  "\<lbrakk> ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; valid_mdb' s \<rbrakk> \<Longrightarrow>
  \<exists>c. ctes_of s (mdbNext (cteMDBNode cte)) = Some c \<and> mdbPrev (cteMDBNode c) = p" by (clarsimp simp add: valid_mdb'_def valid_mdb_ctes_def valid_dlist_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; valid_mdb' s\<rbrakk> \<Longrightarrow> \<exists>c. ctes_of s (mdbNext (cteMDBNode cte)) = Some c \<and> mdbPrev (cteMDBNode c) = p
theory CSpace1_R

lemma valid_mdbD2':
  "\<lbrakk> ctes_of s p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; valid_mdb' s \<rbrakk> \<Longrightarrow>
  \<exists>c. ctes_of s (mdbPrev (cteMDBNode cte)) = Some c \<and> mdbNext (cteMDBNode c) = p" by (clarsimp simp add: valid_mdb'_def valid_mdb_ctes_def valid_dlist_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; valid_mdb' s\<rbrakk> \<Longrightarrow> \<exists>c. ctes_of s (mdbPrev (cteMDBNode cte)) = Some c \<and> mdbNext (cteMDBNode c) = p
theory CSpace1_R

lemma prev_next_update:
  "cteMDBNode_update (mdbNext_update f) (cteMDBNode_update (mdbPrev_update f') x) =
   cteMDBNode_update (mdbPrev_update f') (cteMDBNode_update (mdbNext_update f) x)" apply (cases x) apply (rename_tac cap mdbnode) apply (case_tac mdbnode) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cteMDBNode_update (mdbNext_update f) (cteMDBNode_update (mdbPrev_update f') x) = cteMDBNode_update (mdbPrev_update f') (cteMDBNode_update (mdbNext_update f) x) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. x = CTE x1 x2 \<Longrightarrow> cteMDBNode_update (mdbNext_update f) (cteMDBNode_update (mdbPrev_update f') x) = cteMDBNode_update (mdbPrev_update f') (cteMDBNode_update (mdbNext_update f) x) proof (prove)
goal (1 subgoal):
 1. \<And>cap mdbnode. x = CTE cap mdbnode \<Longrightarrow> cteMDBNode_update (mdbNext_update f) (cteMDBNode_update (mdbPrev_update f') x) = cteMDBNode_update (mdbPrev_update f') (cteMDBNode_update (mdbNext_update f) x) proof (prove)
goal (1 subgoal):
 1. \<And>cap mdbnode x1 x2 x3 x4. \<lbrakk>x = CTE cap mdbnode; mdbnode = MDB x1 x2 x3 x4\<rbrakk> \<Longrightarrow> cteMDBNode_update (mdbNext_update f) (cteMDBNode_update (mdbPrev_update f') x) = cteMDBNode_update (mdbPrev_update f') (cteMDBNode_update (mdbNext_update f) x) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma next_update_lhs:
  "(m(p \<mapsto> cte) \<turnstile> p \<leadsto> x) = (x = mdbNext (cteMDBNode cte))" by (auto simp: mdb_next_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> p \<leadsto> x = (x = mdbNext (cteMDBNode cte))
theory CSpace1_R

lemma mdb_chain_0_modify_map_prev:
  "mdb_chain_0 m \<Longrightarrow> mdb_chain_0 (modify_map m ptr (cteMDBNode_update (mdbPrev_update f)))" unfolding mdb_chain_0_def apply rule apply (rule update_prev_next_trancl) apply (clarsimp simp: modify_map_def dom_def split: option.splits if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chain_0 m \<Longrightarrow> mdb_chain_0 (modify_map m ptr (cteMDBNode_update (mdbPrev_update f))) proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>dom m. m \<turnstile> x \<leadsto>\<^sup>+ 0 \<Longrightarrow> \<forall>x\<in>dom (modify_map m ptr (cteMDBNode_update (mdbPrev_update f))). modify_map m ptr (cteMDBNode_update (mdbPrev_update f)) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom m. m \<turnstile> x \<leadsto>\<^sup>+ 0; x \<in> dom (modify_map m ptr (cteMDBNode_update (mdbPrev_update f)))\<rbrakk> \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbPrev_update f)) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom m. m \<turnstile> x \<leadsto>\<^sup>+ 0; x \<in> dom (modify_map m ptr (cteMDBNode_update (mdbPrev_update f)))\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma mdb_chain_0D:
  "\<lbrakk> mdb_chain_0 m; p \<in> dom m \<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ 0" unfolding mdb_chain_0_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_chain_0 m; p \<in> dom m\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom m. m \<turnstile> x \<leadsto>\<^sup>+ 0; p \<in> dom m\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ 0
theory CSpace1_R

lemma mdb_chain_0_nextD:
  "\<lbrakk> mdb_chain_0 m; m p = Some cte \<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* 0" apply (drule mdb_chain_0D) apply (erule domI) apply (erule tranclE2) apply (simp add: next_unfold') apply (simp add: next_unfold') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_chain_0 m; m p = Some cte\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* 0 proof (prove)
goal (2 subgoals):
 1. m p = Some cte \<Longrightarrow> ?p \<in> dom m
 2. \<lbrakk>m p = Some cte; m \<turnstile> ?p \<leadsto>\<^sup>+ 0\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some cte; m \<turnstile> p \<leadsto>\<^sup>+ 0\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m p = Some cte; m \<turnstile> p \<leadsto> 0\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* 0
 2. \<And>c. \<lbrakk>m p = Some cte; m \<turnstile> p \<leadsto> c; m \<turnstile> c \<leadsto>\<^sup>+ 0\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* 0 proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>m p = Some cte; m \<turnstile> p \<leadsto> c; m \<turnstile> c \<leadsto>\<^sup>+ 0\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* 0 proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma null_mdb_no_next:
  "\<lbrakk> valid_dlist m; no_0 m;
  cte_mdb_prop m target (\<lambda>m. mdbPrev m = nullPointer \<and> mdbNext m = nullPointer) \<rbrakk>
  \<Longrightarrow> \<not> m \<turnstile> x \<leadsto> target" unfolding cte_mdb_prop_def by (auto elim: valid_dlistE elim!: valid_mdb_ctesE
    simp: nullPointer_def no_0_def next_unfold')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist m; no_0 m; cte_mdb_prop m target (\<lambda>m. mdbPrev m = nullPointer \<and> mdbNext m = nullPointer)\<rbrakk> \<Longrightarrow> (x, target) \<notin> mdb_next_rel m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist m; no_0 m; \<exists>cte. m target = Some cte \<and> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> (x, target) \<notin> mdb_next_rel m
theory CSpace1_R

lemma null_mdb_no_trancl:
  "\<lbrakk> valid_dlist m; no_0 m;
  cte_mdb_prop m target (\<lambda>m. mdbPrev m = nullPointer \<and> mdbNext m = nullPointer) \<rbrakk>
  \<Longrightarrow> \<not> m \<turnstile> x \<leadsto>\<^sup>+ target" by (auto dest: null_mdb_no_next elim: tranclE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist m; no_0 m; cte_mdb_prop m target (\<lambda>m. mdbPrev m = nullPointer \<and> mdbNext m = nullPointer)\<rbrakk> \<Longrightarrow> (x, target) \<notin> (mdb_next_rel m)\<^sup>+
theory CSpace1_R

lemma cap_asid_base_update' [simp]:
  "cap_asid_base' (RetypeDecls_H.updateCapData P x c) = cap_asid_base' c" unfolding cap_asid_base'_def apply (cases c, simp_all add: updateCapData_def isCap_simps Let_def) apply (rename_tac arch_capability) apply (case_tac arch_capability,
         simp_all add: updateCapData_def
                       ARM_H.updateCapData_def
                       isCap_simps Let_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_asid_base' (global.updateCapData P x c) = cap_asid_base' c proof (prove)
goal (1 subgoal):
 1. (case global.updateCapData P x c of capability.ArchObjectCap (arch_capability.ASIDPoolCap x asid) \<Rightarrow> Some asid | capability.ArchObjectCap _ \<Rightarrow> None | _ \<Rightarrow> None) = (case c of capability.ArchObjectCap (arch_capability.ASIDPoolCap x asid) \<Rightarrow> Some asid | capability.ArchObjectCap _ \<Rightarrow> None | _ \<Rightarrow> None) proof (prove)
goal (1 subgoal):
 1. \<And>x8. c = capability.ArchObjectCap x8 \<Longrightarrow> (case Arch.updateCapData P x x8 of capability.ArchObjectCap (arch_capability.ASIDPoolCap x asid) \<Rightarrow> Some asid | capability.ArchObjectCap _ \<Rightarrow> None | _ \<Rightarrow> None) = (case x8 of arch_capability.ASIDPoolCap x xa \<Rightarrow> Some xa | _ \<Rightarrow> None) proof (prove)
goal (1 subgoal):
 1. \<And>arch_capability. c = capability.ArchObjectCap arch_capability \<Longrightarrow> (case Arch.updateCapData P x arch_capability of capability.ArchObjectCap (arch_capability.ASIDPoolCap x asid) \<Rightarrow> Some asid | capability.ArchObjectCap _ \<Rightarrow> None | _ \<Rightarrow> None) = (case arch_capability of arch_capability.ASIDPoolCap x xa \<Rightarrow> Some xa | _ \<Rightarrow> None) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma updateCapData_Master:
  "updateCapData P d cap \<noteq> NullCap \<Longrightarrow>
   capMasterCap (updateCapData P d cap) = capMasterCap cap" apply (cases cap, simp_all add: updateCapData_def isCap_simps Let_def
                           split: if_split_asm) apply (rename_tac arch_capability) apply (case_tac arch_capability, simp_all add: ARM_H.updateCapData_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.updateCapData P d cap \<noteq> capability.NullCap \<Longrightarrow> capMasterCap (global.updateCapData P d cap) = capMasterCap cap proof (prove)
goal (1 subgoal):
 1. \<And>x8. \<lbrakk>Arch.updateCapData P d x8 \<noteq> capability.NullCap; cap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> capMasterCap (Arch.updateCapData P d x8) = capMasterCap (capability.ArchObjectCap x8) proof (prove)
goal (1 subgoal):
 1. \<And>arch_capability. \<lbrakk>Arch.updateCapData P d arch_capability \<noteq> capability.NullCap; cap = capability.ArchObjectCap arch_capability\<rbrakk> \<Longrightarrow> capMasterCap (Arch.updateCapData P d arch_capability) = capMasterCap (capability.ArchObjectCap arch_capability) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma updateCapData_Reply:
  "isReplyCap (updateCapData P x c) = isReplyCap c" apply (cases "updateCapData P x c = NullCap") apply (clarsimp simp: isCap_simps) apply (simp add: updateCapData_def isCap_simps Let_def) apply (drule updateCapData_Master) apply (rule master_eqI, rule isCap_Master) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isReplyCap (global.updateCapData P x c) = isReplyCap c proof (prove)
goal (2 subgoals):
 1. global.updateCapData P x c = capability.NullCap \<Longrightarrow> isReplyCap (global.updateCapData P x c) = isReplyCap c
 2. global.updateCapData P x c \<noteq> capability.NullCap \<Longrightarrow> isReplyCap (global.updateCapData P x c) = isReplyCap c proof (prove)
goal (2 subgoals):
 1. \<And>v0 v1 v2. \<lbrakk>global.updateCapData P x (capability.ReplyCap v0 v1 v2) = capability.NullCap; c = capability.ReplyCap v0 v1 v2\<rbrakk> \<Longrightarrow> False
 2. global.updateCapData P x c \<noteq> capability.NullCap \<Longrightarrow> isReplyCap (global.updateCapData P x c) = isReplyCap c proof (prove)
goal (1 subgoal):
 1. global.updateCapData P x c \<noteq> capability.NullCap \<Longrightarrow> isReplyCap (global.updateCapData P x c) = isReplyCap c proof (prove)
goal (1 subgoal):
 1. capMasterCap (global.updateCapData P x c) = capMasterCap c \<Longrightarrow> isReplyCap (global.updateCapData P x c) = isReplyCap c proof (prove)
goal (1 subgoal):
 1. capMasterCap (global.updateCapData P x c) = capMasterCap c \<Longrightarrow> isReplyCap (capMasterCap (global.updateCapData P x c)) = isReplyCap (capMasterCap c) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma weak_derived_updateCapData:
  "\<lbrakk> (updateCapData P x c) \<noteq> NullCap; weak_derived' c c';
      capBadge (updateCapData P x c) = capBadge c' \<rbrakk>
  \<Longrightarrow> weak_derived' (updateCapData P x c) c'" apply (clarsimp simp add: weak_derived'_def updateCapData_Master) apply (clarsimp elim: impE dest!: iffD1[OF updateCapData_Reply]) apply (clarsimp simp: isCap_simps) apply (clarsimp simp: Let_def isCap_simps updateCapData_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.updateCapData P x c \<noteq> capability.NullCap; weak_derived' c c'; capBadge (global.updateCapData P x c) = capBadge c'\<rbrakk> \<Longrightarrow> weak_derived' (global.updateCapData P x c) c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.updateCapData P x c \<noteq> capability.NullCap; capBadge (global.updateCapData P x c) = capBadge c'; capMasterCap c = capMasterCap c'; capBadge c = capBadge c'; capASID c = capASID c'; cap_asid_base' c = cap_asid_base' c'; cap_vptr' c = cap_vptr' c'; isReplyCap c \<longrightarrow> capTCBPtr c = capTCBPtr c' \<and> capReplyMaster c = capReplyMaster c'; isReplyCap (global.updateCapData P x c)\<rbrakk> \<Longrightarrow> capTCBPtr (global.updateCapData P x c) = capTCBPtr c' \<and> capReplyMaster (global.updateCapData P x c) = capReplyMaster c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.updateCapData P x c \<noteq> capability.NullCap; capBadge (global.updateCapData P x c) = capBadge c'; capMasterCap c = capMasterCap c'; capBadge c = capBadge c'; capASID c = capASID c'; cap_asid_base' c = cap_asid_base' c'; cap_vptr' c = cap_vptr' c'; isReplyCap c; capTCBPtr c = capTCBPtr c'; capReplyMaster c = capReplyMaster c'\<rbrakk> \<Longrightarrow> capTCBPtr (global.updateCapData P x c) = capTCBPtr c' \<and> capReplyMaster (global.updateCapData P x c) = capReplyMaster c' proof (prove)
goal (1 subgoal):
 1. \<And>v2 master g. \<lbrakk>global.updateCapData P x (capability.ReplyCap (capTCBPtr c') (capReplyMaster c') v2) \<noteq> capability.NullCap; capBadge (global.updateCapData P x (capability.ReplyCap (capTCBPtr c') (capReplyMaster c') v2)) = None; None = capBadge c'; None = capASID c'; None = cap_asid_base' c'; None = cap_vptr' c'; c = capability.ReplyCap (capTCBPtr c') (capReplyMaster c') v2; c' = capability.ReplyCap (capTCBPtr c') master g\<rbrakk> \<Longrightarrow> capTCBPtr (global.updateCapData P x (capability.ReplyCap (capTCBPtr c') (capReplyMaster c') v2)) = capTCBPtr c' \<and> capReplyMaster (global.updateCapData P x (capability.ReplyCap (capTCBPtr c') (capReplyMaster c') v2)) = capReplyMaster c' proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma maskCapRights_Reply[simp]:
  "isReplyCap (maskCapRights r c) = isReplyCap c" apply (insert capMasterCap_maskCapRights) apply (rule master_eqI, rule isCap_Master) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isReplyCap (global.maskCapRights r c) = isReplyCap c proof (prove)
goal (1 subgoal):
 1. (\<And>msk cap. capMasterCap (global.maskCapRights msk cap) = capMasterCap cap) \<Longrightarrow> isReplyCap (global.maskCapRights r c) = isReplyCap c proof (prove)
goal (1 subgoal):
 1. (\<And>msk cap. capMasterCap (global.maskCapRights msk cap) = capMasterCap cap) \<Longrightarrow> isReplyCap (capMasterCap (global.maskCapRights r c)) = isReplyCap (capMasterCap c) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma cap_asid_base_mask' [simp]:
  "cap_asid_base' (maskCapRights x c) = cap_asid_base' c" unfolding cap_vptr'_def apply (cases c, simp_all add: maskCapRights_def isCap_simps Let_def) apply (rename_tac arch_capability) apply (case_tac arch_capability,
         simp_all add: maskCapRights_def ARM_H.maskCapRights_def isCap_simps Let_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_asid_base' (global.maskCapRights x c) = cap_asid_base' c proof (prove)
goal (1 subgoal):
 1. cap_asid_base' (global.maskCapRights x c) = cap_asid_base' c proof (prove)
goal (1 subgoal):
 1. \<And>x8. c = capability.ArchObjectCap x8 \<Longrightarrow> cap_asid_base' (Arch.maskCapRights x x8) = cap_asid_base' (capability.ArchObjectCap x8) proof (prove)
goal (1 subgoal):
 1. \<And>arch_capability. c = capability.ArchObjectCap arch_capability \<Longrightarrow> cap_asid_base' (Arch.maskCapRights x arch_capability) = cap_asid_base' (capability.ArchObjectCap arch_capability) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma subtree_not_Null:
  assumes null: "m p = Some (CTE capability.NullCap node)"
  assumes sub: "m \<turnstile> c \<rightarrow> p"
  shows "False" using sub null by induct (auto simp: parentOf_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. False proof (prove)
using this:
m \<turnstile> c \<rightarrow> p
m p = Some (CTE capability.NullCap node)

goal (1 subgoal):
 1. False
theory CSpace1_R

lemma Null_not_subtree:
  assumes null: "m c = Some (CTE capability.NullCap node)"
  assumes sub: "m \<turnstile> c \<rightarrow> p"
  shows "False" using sub null by induct (auto simp: parentOf_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. False proof (prove)
using this:
m \<turnstile> c \<rightarrow> p
m c = Some (CTE capability.NullCap node)

goal (1 subgoal):
 1. False
theory CSpace1_R

lemma ps_clear_16:
  "\<lbrakk> ps_clear p tcbBlockSizeBits s; is_aligned p tcbBlockSizeBits \<rbrakk> \<Longrightarrow> ksPSpace s (p + 2^cteSizeBits) = None" apply (simp add: ps_clear_def) apply (drule equals0D[where a="p + 2^cteSizeBits"]) apply (simp add: dom_def add.commute objBits_defs take_bit_Suc) apply (drule mp) apply (rule word_plus_mono_right) apply simp apply (erule is_aligned_no_wrap') apply simp apply (erule mp) apply (erule is_aligned_no_wrap') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps_clear p tcbBlockSizeBits s; is_aligned p tcbBlockSizeBits\<rbrakk> \<Longrightarrow> ksPSpace s (p + 2 ^ cteSizeBits) = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>({p..p + 2 ^ tcbBlockSizeBits - 1} - {p}) \<inter> dom (ksPSpace s) = {}; is_aligned p tcbBlockSizeBits\<rbrakk> \<Longrightarrow> ksPSpace s (p + 2 ^ cteSizeBits) = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p tcbBlockSizeBits; p + 2 ^ cteSizeBits \<notin> ({p..p + 2 ^ tcbBlockSizeBits - 1} - {p}) \<inter> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s (p + 2 ^ cteSizeBits) = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p 9; p + 0x10 \<le> p + 0x1FF \<longrightarrow> p \<le> p + 0x10 \<longrightarrow> ksPSpace s (p + 0x10) = None\<rbrakk> \<Longrightarrow> ksPSpace s (p + 0x10) = None proof (prove)
goal (2 subgoals):
 1. is_aligned p 9 \<Longrightarrow> p + 0x10 \<le> p + 0x1FF
 2. \<lbrakk>is_aligned p 9; p \<le> p + 0x10 \<longrightarrow> ksPSpace s (p + 0x10) = None\<rbrakk> \<Longrightarrow> ksPSpace s (p + 0x10) = None proof (prove)
goal (3 subgoals):
 1. is_aligned p 9 \<Longrightarrow> 0x10 \<le> 0x1FF
 2. is_aligned p 9 \<Longrightarrow> p \<le> p + 0x1FF
 3. \<lbrakk>is_aligned p 9; p \<le> p + 0x10 \<longrightarrow> ksPSpace s (p + 0x10) = None\<rbrakk> \<Longrightarrow> ksPSpace s (p + 0x10) = None proof (prove)
goal (2 subgoals):
 1. is_aligned p 9 \<Longrightarrow> p \<le> p + 0x1FF
 2. \<lbrakk>is_aligned p 9; p \<le> p + 0x10 \<longrightarrow> ksPSpace s (p + 0x10) = None\<rbrakk> \<Longrightarrow> ksPSpace s (p + 0x10) = None proof (prove)
goal (2 subgoals):
 1. 0x1FF < 2 ^ 9
 2. \<lbrakk>is_aligned p 9; p \<le> p + 0x10 \<longrightarrow> ksPSpace s (p + 0x10) = None\<rbrakk> \<Longrightarrow> ksPSpace s (p + 0x10) = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p 9; p \<le> p + 0x10 \<longrightarrow> ksPSpace s (p + 0x10) = None\<rbrakk> \<Longrightarrow> ksPSpace s (p + 0x10) = None proof (prove)
goal (1 subgoal):
 1. is_aligned p 9 \<Longrightarrow> p \<le> p + 0x10 proof (prove)
goal (1 subgoal):
 1. 0x10 < 2 ^ 9 proof (prove)
goal:
No subgoals!