kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_R

lemma m_cap':
  "m p = Some (CTE cap node) \<Longrightarrow>
  \<exists>node'. if p = dest then cap = dest_cap \<and> n' p = Some (CTE c' node')
          else n' p = Some (CTE cap node')" apply (simp add: n'_def n new_src_def new_dest_def modify_map_if) apply (cases "p=dest") apply (auto simp: src dest) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m p = Some (CTE cap node) \<Longrightarrow> \<exists>node'. if p = dest then cap = dest_cap \<and> n' p = Some (CTE c' node') else n' p = Some (CTE cap node') proof (prove)
goal (1 subgoal):
 1. m p = Some (CTE cap node) \<Longrightarrow> (p = src \<longrightarrow> src_cap = cap) \<and> (p \<noteq> src \<longrightarrow> (\<exists>node'. (mdbNext src_node = p \<longrightarrow> (p = dest \<longrightarrow> cap = dest_cap \<and> node' = mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))) \<and> (p \<noteq> dest \<longrightarrow> mdbPrev_update (\<lambda>_. dest) node = node')) \<and> (mdbNext src_node \<noteq> p \<longrightarrow> (p = dest \<longrightarrow> cap = dest_cap \<and> node' = mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))) \<and> (p \<noteq> dest \<longrightarrow> node = node')))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m p = Some (CTE cap node); p = dest\<rbrakk> \<Longrightarrow> (p = src \<longrightarrow> src_cap = cap) \<and> (p \<noteq> src \<longrightarrow> (\<exists>node'. (mdbNext src_node = p \<longrightarrow> (p = dest \<longrightarrow> cap = dest_cap \<and> node' = mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))) \<and> (p \<noteq> dest \<longrightarrow> mdbPrev_update (\<lambda>_. dest) node = node')) \<and> (mdbNext src_node \<noteq> p \<longrightarrow> (p = dest \<longrightarrow> cap = dest_cap \<and> node' = mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))) \<and> (p \<noteq> dest \<longrightarrow> node = node'))))
 2. \<lbrakk>m p = Some (CTE cap node); p \<noteq> dest\<rbrakk> \<Longrightarrow> (p = src \<longrightarrow> src_cap = cap) \<and> (p \<noteq> src \<longrightarrow> (\<exists>node'. (mdbNext src_node = p \<longrightarrow> (p = dest \<longrightarrow> cap = dest_cap \<and> node' = mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))) \<and> (p \<noteq> dest \<longrightarrow> mdbPrev_update (\<lambda>_. dest) node = node')) \<and> (mdbNext src_node \<noteq> p \<longrightarrow> (p = dest \<longrightarrow> cap = dest_cap \<and> node' = mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))) \<and> (p \<noteq> dest \<longrightarrow> node = node')))) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma descendants':
  "descendants_of' p n' =
   (if src \<in> descendants_of' p m \<or> p = src
   then descendants_of' p m \<union> {dest} else descendants_of' p m)" by (simp add: n'_def descendants descendants_of_prev_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of' p n' = (if src \<in> descendants_of' p m \<or> p = src then descendants_of' p m \<union> {dest} else descendants_of' p m)
theory CSpace_R

lemma m_prev_of_next:
  "m \<turnstile> p \<leftarrow> mdbNext src_node = (p = src \<and> mdbNext src_node \<noteq> 0)" using src apply (clarsimp simp: mdb_prev_def) apply (rule iffI) apply clarsimp apply (rule dlistEn, assumption, clarsimp) apply clarsimp apply clarsimp apply (rule dlistEn, assumption, clarsimp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p \<leftarrow> mdbNext src_node = (p = src \<and> mdbNext src_node \<noteq> 0) proof (prove)
using this:
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. m \<turnstile> p \<leftarrow> mdbNext src_node = (p = src \<and> mdbNext src_node \<noteq> 0) proof (prove)
goal (1 subgoal):
 1. m src = Some (CTE src_cap src_node) \<Longrightarrow> (\<exists>z. m (mdbNext src_node) = Some z \<and> p = mdbPrev (cteMDBNode z)) = (p = src \<and> mdbNext src_node \<noteq> 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); \<exists>z. m (mdbNext src_node) = Some z \<and> p = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> p = src \<and> mdbNext src_node \<noteq> 0
 2. \<lbrakk>m src = Some (CTE src_cap src_node); p = src \<and> mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>z. m (mdbNext src_node) = Some z \<and> p = mdbPrev (cteMDBNode z) proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>m src = Some (CTE src_cap src_node); m (mdbNext src_node) = Some z; p = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode z) = src \<and> mdbNext src_node \<noteq> 0
 2. \<lbrakk>m src = Some (CTE src_cap src_node); p = src \<and> mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>z. m (mdbNext src_node) = Some z \<and> p = mdbPrev (cteMDBNode z) proof (prove)
goal (2 subgoals):
 1. \<And>z cte'. \<lbrakk>m src = Some (CTE src_cap src_node); m (mdbNext src_node) = Some z; p = mdbPrev (cteMDBNode z); m (mdbNext (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbPrev (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode z) = src \<and> mdbNext src_node \<noteq> 0
 2. \<lbrakk>m src = Some (CTE src_cap src_node); p = src \<and> mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>z. m (mdbNext src_node) = Some z \<and> p = mdbPrev (cteMDBNode z) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); p = src \<and> mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>z. m (mdbNext src_node) = Some z \<and> p = mdbPrev (cteMDBNode z) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); p = src; mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>z. m (mdbNext src_node) = Some z \<and> src = mdbPrev (cteMDBNode z) proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>m src = Some (CTE src_cap src_node); p = src; mdbNext src_node \<noteq> 0; m (mdbNext (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbPrev (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> \<exists>z. m (mdbNext src_node) = Some z \<and> src = mdbPrev (cteMDBNode z) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma src_next_eq':
  "m (mdbNext src_node) = Some cte \<Longrightarrow> m \<turnstile> p \<leadsto> mdbNext src_node = (p = src)" by (subst src_next_eq) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m (mdbNext src_node) = Some cte \<Longrightarrow> m \<turnstile> p \<leadsto> mdbNext src_node = (p = src)
theory CSpace_R

lemma src_prev [iff]:
  "m \<turnstile> src \<leftarrow> p = (p = mdbNext src_node \<and> p \<noteq> 0)" using src apply - apply (rule iffI) prefer 2 apply (clarsimp simp: mdb_ptr_src.next_p_prev) apply (clarsimp simp: mdb_prev_def) apply (rule conjI) prefer 2 apply clarsimp apply (rule dlistEp [where p=p], assumption, clarsimp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> src \<leftarrow> p = (p = mdbNext src_node \<and> p \<noteq> 0) proof (prove)
using this:
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. m \<turnstile> src \<leftarrow> p = (p = mdbNext src_node \<and> p \<noteq> 0) proof (prove)
goal (1 subgoal):
 1. m src = Some (CTE src_cap src_node) \<Longrightarrow> m \<turnstile> src \<leftarrow> p = (p = mdbNext src_node \<and> p \<noteq> 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m \<turnstile> src \<leftarrow> p\<rbrakk> \<Longrightarrow> p = mdbNext src_node \<and> p \<noteq> 0
 2. \<lbrakk>m src = Some (CTE src_cap src_node); p = mdbNext src_node \<and> p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leftarrow> p proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); p = mdbNext src_node \<and> p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leftarrow> p
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m \<turnstile> src \<leftarrow> p\<rbrakk> \<Longrightarrow> p = mdbNext src_node \<and> p \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m \<turnstile> src \<leftarrow> p\<rbrakk> \<Longrightarrow> p = mdbNext src_node \<and> p \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>m (mdbPrev (cteMDBNode z)) = Some (CTE src_cap src_node); m p = Some z; src = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> p = mdbNext src_node \<and> p \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>m (mdbPrev (cteMDBNode z)) = Some (CTE src_cap src_node); m p = Some z; src = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> p = mdbNext src_node
 2. \<And>z. \<lbrakk>m (mdbPrev (cteMDBNode z)) = Some (CTE src_cap src_node); m p = Some z; src = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> p \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>m (mdbPrev (cteMDBNode z)) = Some (CTE src_cap src_node); m p = Some z; src = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> p \<noteq> 0
 2. \<And>z. \<lbrakk>m (mdbPrev (cteMDBNode z)) = Some (CTE src_cap src_node); m p = Some z; src = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> p = mdbNext src_node proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>m (mdbPrev (cteMDBNode z)) = Some (CTE src_cap src_node); m p = Some z; src = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> p = mdbNext src_node proof (prove)
goal (1 subgoal):
 1. \<And>z cte'. \<lbrakk>m (mdbPrev (cteMDBNode z)) = Some (CTE src_cap src_node); m p = Some z; src = mdbPrev (cteMDBNode z); m (mdbPrev (cteMDBNode z)) = Some cte'; mdbNext (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> p = mdbNext src_node proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma utRange_c':
  "untypedRange c' \<subseteq> untypedRange src_cap" using safe_parent src by - (drule (1) safe_parent_for_untypedRange, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untypedRange c' \<subseteq> untypedRange src_cap proof (prove)
using this:
safe_parent_for' m src c'
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. untypedRange c' \<subseteq> untypedRange src_cap
theory CSpace_R

lemma capRange_c':
  "capRange c' \<subseteq> capRange src_cap" using safe_parent src by - (drule (1) safe_parent_for_capRange_capBits, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capRange c' \<subseteq> capRange src_cap proof (prove)
using this:
safe_parent_for' m src c'
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. capRange c' \<subseteq> capRange src_cap
theory CSpace_R

lemma not_ut_c' [simp]:
  "\<not>isUntypedCap c'" using simple by (simp add: is_simple_cap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> isUntypedCap c' proof (prove)
using this:
is_simple_cap' c'

goal (1 subgoal):
 1. \<not> isUntypedCap c'
theory CSpace_R

lemma utCapRange_c':
  "capRange c' \<subseteq> untypedRange src_cap" using safe_parent src by - (drule (1) safe_parent_for_capUntypedRange, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capRange c' \<subseteq> untypedRange src_cap proof (prove)
using this:
safe_parent_for' m src c'
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. capRange c' \<subseteq> untypedRange src_cap
theory CSpace_R

lemma ut_descendants:
  "isUntypedCap src_cap \<Longrightarrow> descendants_of' src m = {}" using safe_parent src by (rule safe_parent_for_descendants')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isUntypedCap src_cap \<Longrightarrow> descendants_of' src m = {} proof (prove)
using this:
safe_parent_for' m src c'
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. isUntypedCap src_cap \<Longrightarrow> descendants_of' src m = {}
theory CSpace_R

lemma n'_badge:
  "n' p = Some (CTE cap node) \<Longrightarrow>
  \<exists>node'. if p = dest then mdbFirstBadged node = revokable' src_cap c' \<and> m p = Some (CTE dest_cap node')
          else m p = Some (CTE cap node') \<and> mdbFirstBadged node = mdbFirstBadged node'" by (auto simp add: n'_def n src dest new_src_def new_dest_def modify_map_if split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n' p = Some (CTE cap node) \<Longrightarrow> \<exists>node'. if p = dest then mdbFirstBadged node = revokable' src_cap c' \<and> m p = Some (CTE dest_cap node') else m p = Some (CTE cap node') \<and> mdbFirstBadged node = mdbFirstBadged node'
theory CSpace_R

lemma src_not_ep [simp]:
  "\<not>isEndpointCap src_cap" using safe_parent src by (rule safe_parent_not_ep')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> isEndpointCap src_cap proof (prove)
using this:
safe_parent_for' m src c'
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. \<not> isEndpointCap src_cap
theory CSpace_R

lemma src_not_ntfn [simp]:
  "\<not>isNotificationCap src_cap" using safe_parent src by (rule safe_parent_not_ntfn')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> isNotificationCap src_cap proof (prove)
using this:
safe_parent_for' m src c'
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. \<not> isNotificationCap src_cap
theory CSpace_R

lemma c_not_ep [simp]:
  "\<not>isEndpointCap c'" using simple by (simp add: is_simple_cap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> isEndpointCap c' proof (prove)
using this:
is_simple_cap' c'

goal (1 subgoal):
 1. \<not> isEndpointCap c'
theory CSpace_R

lemma c_not_ntfn [simp]:
  "\<not>isNotificationCap c'" using simple by (simp add: is_simple_cap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> isNotificationCap c' proof (prove)
using this:
is_simple_cap' c'

goal (1 subgoal):
 1. \<not> isNotificationCap c'
theory CSpace_R

lemma capClass_c' [simp]:
  "capClass c' = capClass src_cap" using safe_parent src by (rule safe_parent_capClass)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capClass c' = capClass src_cap proof (prove)
using this:
safe_parent_for' m src c'
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. capClass c' = capClass src_cap
theory CSpace_R

lemma sameRegion_src [simp]:
  "sameRegionAs src_cap c'" using safe_parent src apply (simp add: safe_parent_for'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.sameRegionAs src_cap c' proof (prove)
using this:
safe_parent_for' m src c'
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. global.sameRegionAs src_cap c' proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma irq_c'_new:
  assumes irq_src: "isIRQControlCap src_cap"
  shows "m p = Some (CTE cap node) \<Longrightarrow> \<not> sameRegionAs c' cap" using safe_parent irq_src src apply (clarsimp simp: safe_parent_for'_def isCap_simps) apply (clarsimp simp: sameRegionAs_def2 isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m p = Some (CTE cap node) \<Longrightarrow> \<not> global.sameRegionAs c' cap proof (prove)
using this:
safe_parent_for' m src c'
isIRQControlCap src_cap
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. m p = Some (CTE cap node) \<Longrightarrow> \<not> global.sameRegionAs c' cap proof (prove)
goal (1 subgoal):
 1. \<And>irq. \<lbrakk>m p = Some (CTE cap node); src_cap = capability.IRQControlCap; m src = Some (CTE capability.IRQControlCap src_node); \<forall>p n'. m p \<noteq> Some (CTE (capability.IRQHandlerCap irq) n'); c' = capability.IRQHandlerCap irq; global.sameRegionAs (capability.IRQHandlerCap irq) cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma not_irq_parentD:
  "\<not> isIRQControlCap src_cap \<Longrightarrow>
  isUntypedCap src_cap \<and> descendants_of' src m = {} \<and> capRange c' \<noteq> {}" using src safe_parent unfolding safe_parent_for'_def by (clarsimp simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> isIRQControlCap src_cap \<Longrightarrow> isUntypedCap src_cap \<and> descendants_of' src m = {} \<and> capRange c' \<noteq> {} proof (prove)
using this:
m src = Some (CTE src_cap src_node)
safe_parent_for' m src c'

goal (1 subgoal):
 1. \<not> isIRQControlCap src_cap \<Longrightarrow> isUntypedCap src_cap \<and> descendants_of' src m = {} \<and> capRange c' \<noteq> {} proof (prove)
using this:
m src = Some (CTE src_cap src_node)
\<exists>parent node. m src = Some (CTE parent node) \<and> global.sameRegionAs parent c' \<and> ((\<exists>irq. c' = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. m p \<noteq> Some (CTE c' n')) \<or> isUntypedCap parent \<and> descendants_of' src m = {} \<and> capRange c' \<noteq> {} \<and> capBits c' \<le> capBits parent)

goal (1 subgoal):
 1. \<not> isIRQControlCap src_cap \<Longrightarrow> isUntypedCap src_cap \<and> descendants_of' src m = {} \<and> capRange c' \<noteq> {}
theory CSpace_R

lemma ut_src:
  "\<lbrakk> isUntypedCap src_cap; sameRegionAs cap c'; m p = Some (CTE cap node) \<rbrakk> \<Longrightarrow>
  isUntypedCap cap \<and> untypedRange cap \<inter> untypedRange src_cap \<noteq> {}" apply (frule (2) ut_src_only_ut_c_parents) apply simp apply (frule sameRegion_capRange_sub) apply (insert utCapRange_c')[1] apply (simp add: untypedCapRange) apply (drule ut_capRange_non_empty) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node)\<rbrakk> \<Longrightarrow> isUntypedCap cap \<and> untypedRange cap \<inter> untypedRange src_cap \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); isUntypedCap cap\<rbrakk> \<Longrightarrow> isUntypedCap cap \<and> untypedRange cap \<inter> untypedRange src_cap \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); isUntypedCap cap\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> untypedRange src_cap \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); isUntypedCap cap; capRange c' \<subseteq> capRange cap\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> untypedRange src_cap \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); isUntypedCap cap; capRange c' \<subseteq> capRange cap; capRange c' \<subseteq> untypedRange src_cap\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> untypedRange src_cap \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap src_cap; global.sameRegionAs cap c'; m p = Some (CTE cap node); isUntypedCap cap; capRange c' \<subseteq> untypedRange cap; capRange c' \<subseteq> untypedRange src_cap\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> untypedRange src_cap \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.sameRegionAs cap c'; m p = Some (CTE cap node); isUntypedCap cap; capRange c' \<subseteq> untypedRange cap; capRange c' \<subseteq> untypedRange src_cap; capRange c' \<noteq> {}\<rbrakk> \<Longrightarrow> untypedRange cap \<inter> untypedRange src_cap \<noteq> {} proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma notArchPage:
  "\<not> isArchPageCap c'" using simple by (clarsimp simp: isCap_simps is_simple_cap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> isArchPageCap c' proof (prove)
using this:
is_simple_cap' c'

goal (1 subgoal):
 1. \<not> isArchPageCap c'
theory CSpace_R

lemma reply_masters_rvk_fb:
  "reply_masters_rvk_fb m" using valid by (simp add: valid_mdb_ctes_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_masters_rvk_fb m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. reply_masters_rvk_fb m
theory CSpace_R

lemma mdb:
  "valid_mdb_ctes n'" by (simp add: valid_mdb_ctes_def no_0_n' chain_n')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb_ctes n'
theory CSpace_R

lemma ensureEmptySlot_stronger [wp]:
  "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>c. cteCap c = NullCap) p s \<longrightarrow> P s\<rbrace> ensureEmptySlot p \<lbrace>\<lambda>rv. P\<rbrace>, -" apply (simp add: ensureEmptySlot_def whenE_def unlessE_whenE) apply (wp getCTE_wp') apply (clarsimp simp: cte_wp_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) p s \<longrightarrow> P s\<rbrace> ensureEmptySlot p \<lbrace>\<lambda>rv. P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) p s \<longrightarrow> P s\<rbrace> doE cte <- liftE (getCTE p);
if cteCap cte \<noteq> capability.NullCap then throwError Fault_H.syscall_error.DeleteFirst else returnOk ()
odE \<lbrace>\<lambda>rv. P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) p s \<longrightarrow> P s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) p s \<longrightarrow> (cteCap cte \<noteq> capability.NullCap \<longrightarrow> True) \<and> (\<not> cteCap cte \<noteq> capability.NullCap \<longrightarrow> P s) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma lookupSlotForCNodeOp_real_cte_at'[wp]:
  "\<lbrace>valid_objs' and valid_cap' rootCap\<rbrace>
     lookupSlotForCNodeOp isSrc rootCap cref depth
   \<lbrace>\<lambda>rv. real_cte_at' rv\<rbrace>,-" apply (simp add: lookupSlotForCNodeOp_def split_def unlessE_def
                     split del: if_split cong: if_cong) apply (rule hoare_pre) apply (wp resolveAddressBits_real_cte_at' | simp | wp (once) hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' rootCap\<rbrace> lookupSlotForCNodeOp isSrc rootCap cref depth \<lbrace>real_cte_at'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' rootCap\<rbrace> if isCNodeCap rootCap then doE y <- rangeCheck depth (Suc 0) (size cref);
lookupErrorOnFailure isSrc (doE result <- CSpace_H.resolveAddressBits rootCap cref depth;
if snd result = 0 then returnOk (fst result) else throwError (Fault_H.lookup_failure.DepthMismatch (snd result) 0)
odE)
odE else throwError (Fault_H.syscall_error.FailedLookup isSrc Fault_H.lookup_failure.InvalidRoot) \<lbrace>real_cte_at'\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'7\<rbrace> if isCNodeCap rootCap then doE y <- rangeCheck depth (Suc 0) (size cref);
lookupErrorOnFailure isSrc (doE result <- CSpace_H.resolveAddressBits rootCap cref depth;
if snd result = 0 then returnOk (fst result) else throwError (Fault_H.lookup_failure.DepthMismatch (snd result) 0)
odE)
odE else throwError (Fault_H.syscall_error.FailedLookup isSrc Fault_H.lookup_failure.InvalidRoot) \<lbrace>real_cte_at'\<rbrace>, -
 2. \<And>s. (valid_objs' and valid_cap' rootCap) s \<Longrightarrow> ?P'7 s proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma cte_refs_maskCapRights[simp]:
  "cte_refs' (maskCapRights rghts cap) = cte_refs' cap" by (rule ext, cases cap,
      simp_all add: maskCapRights_def isCap_defs Let_def
                    ARM_H.maskCapRights_def
         split del: if_split
             split: arch_capability.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_refs' (global.maskCapRights rghts cap) = cte_refs' cap