theory CSpace_R

lemma setupReplyMaster_ifunsafe'[wp]:
  "slot = t + 2 ^ objBits (undefined :: cte) * tcbReplySlot \<Longrightarrow>
   \<lbrace>if_unsafe_then_cap' and ex_cte_cap_to' slot\<rbrace>
     setupReplyMaster t
   \<lbrace>\<lambda>rv s. if_unsafe_then_cap' s\<rbrace>" apply (simp add: ifunsafe'_def3 setupReplyMaster_def locateSlot_conv) apply (wp getCTE_wp') apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of cteCaps_of_def
                        cte_level_bits_def objBits_simps') apply (drule_tac x=crefa in spec) apply (rule conjI) apply clarsimp apply (rule_tac x=cref in exI, fastforce) apply clarsimp apply (rule_tac x=cref' in exI, fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slot = t + 2 ^ objBits undefined * tcbReplySlot \<Longrightarrow> \<lbrace>if_unsafe_then_cap' and ex_cte_cap_wp_to' (\<lambda>_. True) slot\<rbrace> setupReplyMaster t \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. slot = t + 2 ^ objBits undefined * tcbReplySlot \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) and ex_cte_cap_wp_to' (\<lambda>_. True) (t + 2 ^ objBits undefined * tcbReplySlot)\<rbrace> do oldCTE <- getCTE (t + 2 ^ cte_level_bits * tcbReplySlot);
when (cteCap oldCTE = capability.NullCap) (do y <- stateAssert (noReplyCapsFor t) [];
setCTE (t + 2 ^ cte_level_bits * tcbReplySlot) (CTE (capability.ReplyCap t True True) (mdbFirstBadged_update (\<lambda>_. True) (mdbRevocable_update (\<lambda>_. True) nullMDBNode)))
od)
od \<lbrace>\<lambda>rv s. \<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; ((\<lambda>s. \<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) and ex_cte_cap_wp_to' (\<lambda>_. True) (t + 2 ^ objBits undefined * tcbReplySlot)) s\<rbrakk> \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> (if cteCap cte = capability.NullCap then \<lambda>s. noReplyCapsFor t s \<longrightarrow> (\<forall>cref. (\<exists>cap. ((cteCaps_of s)(t + 2 ^ cte_level_bits * tcbReplySlot \<mapsto> cteCap (CTE (capability.ReplyCap t True True) (mdbFirstBadged_update (\<lambda>_. True) (mdbRevocable_update (\<lambda>_. True) nullMDBNode))))) cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. ((cteCaps_of s)(t + 2 ^ cte_level_bits * tcbReplySlot \<mapsto> cteCap (CTE (capability.ReplyCap t True True) (mdbFirstBadged_update (\<lambda>_. True) (mdbRevocable_update (\<lambda>_. True) nullMDBNode))))) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) else (\<lambda>s. \<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)))) s proof (prove)
goal (1 subgoal):
 1. \<And>s cte cref ctea crefa. \<lbrakk>slot = t + 0x10 * tcbReplySlot; \<forall>cref. (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)); ctes_of s cref = Some ctea; t + 0x10 * tcbReplySlot \<in> cte_refs' (cteCap ctea) (irq_node' s); cteCap cte = capability.NullCap; ctes_of s (t + 0x10 * tcbReplySlot) = Some cte; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> (crefa = t + 0x10 * tcbReplySlot \<longrightarrow> (\<exists>cref'. cref' \<noteq> t + 0x10 * tcbReplySlot \<and> (cref' \<noteq> t + 0x10 * tcbReplySlot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> t + 0x10 * tcbReplySlot \<in> cte_refs' cap' (irq_node' s))))) \<and> (crefa \<noteq> t + 0x10 * tcbReplySlot \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. cref' \<noteq> t + 0x10 * tcbReplySlot \<and> (cref' \<noteq> t + 0x10 * tcbReplySlot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cref ctea crefa. \<lbrakk>slot = t + 0x10 * tcbReplySlot; ctes_of s cref = Some ctea; t + 0x10 * tcbReplySlot \<in> cte_refs' (cteCap ctea) (irq_node' s); cteCap cte = capability.NullCap; ctes_of s (t + 0x10 * tcbReplySlot) = Some cte; noReplyCapsFor t s; (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))\<rbrakk> \<Longrightarrow> (crefa = t + 0x10 * tcbReplySlot \<longrightarrow> (\<exists>cref'. cref' \<noteq> t + 0x10 * tcbReplySlot \<and> (cref' \<noteq> t + 0x10 * tcbReplySlot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> t + 0x10 * tcbReplySlot \<in> cte_refs' cap' (irq_node' s))))) \<and> (crefa \<noteq> t + 0x10 * tcbReplySlot \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. cref' \<noteq> t + 0x10 * tcbReplySlot \<and> (cref' \<noteq> t + 0x10 * tcbReplySlot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cref ctea crefa. \<lbrakk>slot = t + 0x10 * tcbReplySlot; ctes_of s cref = Some ctea; t + 0x10 * tcbReplySlot \<in> cte_refs' (cteCap ctea) (irq_node' s); cteCap cte = capability.NullCap; ctes_of s (t + 0x10 * tcbReplySlot) = Some cte; noReplyCapsFor t s; (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))\<rbrakk> \<Longrightarrow> crefa = t + 0x10 * tcbReplySlot \<longrightarrow> (\<exists>cref'. cref' \<noteq> t + 0x10 * tcbReplySlot \<and> (cref' \<noteq> t + 0x10 * tcbReplySlot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> t + 0x10 * tcbReplySlot \<in> cte_refs' cap' (irq_node' s))))
 2. \<And>s cte cref ctea crefa. \<lbrakk>slot = t + 0x10 * tcbReplySlot; ctes_of s cref = Some ctea; t + 0x10 * tcbReplySlot \<in> cte_refs' (cteCap ctea) (irq_node' s); cteCap cte = capability.NullCap; ctes_of s (t + 0x10 * tcbReplySlot) = Some cte; noReplyCapsFor t s; (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))\<rbrakk> \<Longrightarrow> crefa \<noteq> t + 0x10 * tcbReplySlot \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. cref' \<noteq> t + 0x10 * tcbReplySlot \<and> (cref' \<noteq> t + 0x10 * tcbReplySlot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cref ctea. \<lbrakk>slot = t + 0x10 * tcbReplySlot; ctes_of s cref = Some ctea; t + 0x10 * tcbReplySlot \<in> cte_refs' (cteCap ctea) (irq_node' s); cteCap cte = capability.NullCap; ctes_of s (t + 0x10 * tcbReplySlot) = Some cte; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> t + 0x10 * tcbReplySlot \<and> (cref' \<noteq> t + 0x10 * tcbReplySlot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> t + 0x10 * tcbReplySlot \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s cte cref ctea crefa. \<lbrakk>slot = t + 0x10 * tcbReplySlot; ctes_of s cref = Some ctea; t + 0x10 * tcbReplySlot \<in> cte_refs' (cteCap ctea) (irq_node' s); cteCap cte = capability.NullCap; ctes_of s (t + 0x10 * tcbReplySlot) = Some cte; noReplyCapsFor t s; (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))\<rbrakk> \<Longrightarrow> crefa \<noteq> t + 0x10 * tcbReplySlot \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. cref' \<noteq> t + 0x10 * tcbReplySlot \<and> (cref' \<noteq> t + 0x10 * tcbReplySlot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cref ctea crefa. \<lbrakk>slot = t + 0x10 * tcbReplySlot; ctes_of s cref = Some ctea; t + 0x10 * tcbReplySlot \<in> cte_refs' (cteCap ctea) (irq_node' s); cteCap cte = capability.NullCap; ctes_of s (t + 0x10 * tcbReplySlot) = Some cte; noReplyCapsFor t s; (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))\<rbrakk> \<Longrightarrow> crefa \<noteq> t + 0x10 * tcbReplySlot \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s crefa = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. cref' \<noteq> t + 0x10 * tcbReplySlot \<and> (cref' \<noteq> t + 0x10 * tcbReplySlot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cref ctea crefa z cref' za. \<lbrakk>slot = t + 0x10 * tcbReplySlot; ctes_of s cref = Some ctea; t + 0x10 * tcbReplySlot \<in> cte_refs' (cteCap ctea) (irq_node' s); cteCap cte = capability.NullCap; ctes_of s (t + 0x10 * tcbReplySlot) = Some cte; noReplyCapsFor t s; crefa \<noteq> t + 0x10 * tcbReplySlot; cteCap z \<noteq> capability.NullCap; ctes_of s crefa = Some z; crefa \<in> cte_refs' (cteCap za) (irq_node' s); ctes_of s cref' = Some za\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> t + 0x10 * tcbReplySlot \<and> (cref' \<noteq> t + 0x10 * tcbReplySlot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> crefa \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal:
No subgoals!