theory Untyped_R

lemma insertNewCap_ifunsafe'[wp]:
  "\<lbrace>if_unsafe_then_cap' and ex_cte_cap_to' slot\<rbrace>
     insertNewCap parent slot cap
   \<lbrace>\<lambda>rv s. if_unsafe_then_cap' s\<rbrace>" apply (simp add: insertNewCap_def) apply (rule hoare_pre) apply (wp getCTE_wp' | clarsimp simp: ifunsafe'_def3)+ apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of cteCaps_of_def) apply (drule_tac x=cref in spec) apply (rule conjI) apply clarsimp apply (rule_tac x=crefa in exI, fastforce) apply clarsimp apply (rule_tac x=cref' in exI, fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap' and ex_cte_cap_wp_to' (\<lambda>_. True) slot\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap' and ex_cte_cap_wp_to' (\<lambda>_. True) slot\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE parent);
oldCTE <- getCTE slot;
y <- assert (cteCap oldCTE = capability.NullCap \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE parent);
oldCTE <- getCTE slot;
y <- assert (cteCap oldCTE = capability.NullCap \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>
 2. \<And>s. (if_unsafe_then_cap' and ex_cte_cap_wp_to' (\<lambda>_. True) slot) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea cref. \<lbrakk>\<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)); ex_cte_cap_wp_to' (\<lambda>_. True) slot s; cte_wp_at' ((=) cte) parent s; cte_wp_at' ((=) ctea) slot s; cteCap ctea = capability.NullCap; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer\<rbrakk> \<Longrightarrow> (cref = slot \<longrightarrow> cap \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref'. (cref' = slot \<longrightarrow> slot \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> slot \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> slot \<in> cte_refs' cap' (irq_node' s))))) \<and> (cref \<noteq> slot \<longrightarrow> (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = slot \<longrightarrow> cref \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> slot \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea cref crefa cteb. \<lbrakk>\<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 parent = Some cte; ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; ctes_of s crefa = Some cteb; slot \<in> cte_refs' (cteCap cteb) (irq_node' s)\<rbrakk> \<Longrightarrow> (cref = slot \<longrightarrow> cap \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref'. (cref' = slot \<longrightarrow> slot \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> slot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> slot \<in> cte_refs' cap' (irq_node' s))))) \<and> (cref \<noteq> slot \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = slot \<longrightarrow> cref \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> slot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s))))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea cref crefa cteb. \<lbrakk>ctes_of s parent = Some cte; ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; ctes_of s crefa = Some cteb; slot \<in> cte_refs' (cteCap cteb) (irq_node' s); (\<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))\<rbrakk> \<Longrightarrow> (cref = slot \<longrightarrow> cap \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref'. (cref' = slot \<longrightarrow> slot \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> slot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> slot \<in> cte_refs' cap' (irq_node' s))))) \<and> (cref \<noteq> slot \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = slot \<longrightarrow> cref \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> slot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s))))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea cref crefa cteb. \<lbrakk>ctes_of s parent = Some cte; ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; ctes_of s crefa = Some cteb; slot \<in> cte_refs' (cteCap cteb) (irq_node' s); (\<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))\<rbrakk> \<Longrightarrow> cref = slot \<longrightarrow> cap \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref'. (cref' = slot \<longrightarrow> slot \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> slot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> slot \<in> cte_refs' cap' (irq_node' s))))
 2. \<And>s cte ctea cref crefa cteb. \<lbrakk>ctes_of s parent = Some cte; ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; ctes_of s crefa = Some cteb; slot \<in> cte_refs' (cteCap cteb) (irq_node' s); (\<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))\<rbrakk> \<Longrightarrow> cref \<noteq> slot \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = slot \<longrightarrow> cref \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> slot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea crefa cteb. \<lbrakk>ctes_of s parent = Some cte; ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; ctes_of s crefa = Some cteb; slot \<in> cte_refs' (cteCap cteb) (irq_node' s); cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = slot \<longrightarrow> slot \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> slot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> slot \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s cte ctea cref crefa cteb. \<lbrakk>ctes_of s parent = Some cte; ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; ctes_of s crefa = Some cteb; slot \<in> cte_refs' (cteCap cteb) (irq_node' s); (\<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))\<rbrakk> \<Longrightarrow> cref \<noteq> slot \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = slot \<longrightarrow> cref \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> slot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea cref crefa cteb. \<lbrakk>ctes_of s parent = Some cte; ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; ctes_of s crefa = Some cteb; slot \<in> cte_refs' (cteCap cteb) (irq_node' s); (\<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))\<rbrakk> \<Longrightarrow> cref \<noteq> slot \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s cref = Some z \<and> cteCap z = cap) \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = slot \<longrightarrow> cref \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> slot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea cref crefa cteb z cref' za. \<lbrakk>ctes_of s parent = Some cte; ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; ctes_of s crefa = Some cteb; slot \<in> cte_refs' (cteCap cteb) (irq_node' s); cref \<noteq> slot; cteCap z \<noteq> capability.NullCap; ctes_of s cref = Some z; cref \<in> cte_refs' (cteCap za) (irq_node' s); ctes_of s cref' = Some za\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = slot \<longrightarrow> cref \<in> cte_refs' cap (irq_node' s)) \<and> (cref' \<noteq> slot \<longrightarrow> (\<exists>cap'. (\<exists>z. ctes_of s cref' = Some z \<and> cteCap z = cap') \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal:
No subgoals!