theory CSpace1_R

lemma cteInsert_weak_cte_wp_at:
  "\<lbrace>\<lambda>s. if p = dest then P cap else p \<noteq> src \<and>
        cte_wp_at' (\<lambda>c. P (cteCap c)) p s\<rbrace>
   cteInsert cap src dest
   \<lbrace>\<lambda>uu. cte_wp_at'(\<lambda>c. P (cteCap c)) p\<rbrace>" unfolding cteInsert_def error_def updateCap_def setUntypedCapAsFull_def apply (simp add: bind_assoc split del: if_split) apply (wp setCTE_weak_cte_wp_at updateMDB_weak_cte_wp_at hoare_weak_lift_imp | simp)+ apply (wp getCTE_ctes_wp)+ apply (clarsimp simp: isCap_simps split:if_split_asm| rule conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if p = dest then P cap else p \<noteq> src \<and> cte_wp_at' (\<lambda>c. P (cteCap c)) p s\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>uu. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if p = dest then P cap else p \<noteq> src \<and> cte_wp_at' (\<lambda>c. P (cteCap c)) p s\<rbrace> do srcCTE <- getCTE src;
srcMDB <- return (cteMDBNode srcCTE);
srcCap <- return (cteCap srcCTE);
newCapIsRevocable <- return (global.isCapRevocable cap srcCap);
newMDB <- return (mdbFirstBadged_update (\<lambda>_. newCapIsRevocable) (mdbRevocable_update (\<lambda>_. newCapIsRevocable) (mdbPrev_update (\<lambda>_. src) srcMDB)));
oldCTE <- getCTE dest;
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
if isUntypedCap srcCap \<and> isUntypedCap cap \<and> capPtr srcCap = capPtr cap \<and> capBlockSize srcCap = capBlockSize cap then do cte <- getCTE src;
setCTE src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. maxFreeIndex (capBlockSize srcCap)) srcCap) cte)
od else return ();
do cte <- getCTE dest;
setCTE dest (cteCap_update (\<lambda>_. cap) cte)
od;
updateMDB dest (const newMDB);
updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext newMDB) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>uu. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if p = dest then P cap else p \<noteq> src \<and> cte_wp_at' (\<lambda>c. P (cteCap c)) p s\<rbrace> do srcCTE <- getCTE src;
oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
y <- if isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap then do cte <- getCTE src;
setCTE src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. maxFreeIndex (capBlockSize cap)) (cteCap srcCTE)) cte)
od else return ();
x <- getCTE dest;
y <- setCTE dest (cteCap_update (\<lambda>_. cap) x);
y <- updateMDB dest (const (mdbFirstBadged_update (\<lambda>_. global.isCapRevocable cap (cteCap srcCTE)) (mdbRevocable_update (\<lambda>_. global.isCapRevocable cap (cteCap srcCTE)) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))));
y <- updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode srcCTE)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>uu. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>srcCTE. \<lbrace>?P'112 srcCTE\<rbrace> getCTE dest \<lbrace>\<lambda>rv s. mdbPrev (cteMDBNode rv) = nullPointer \<and> mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> cteCap rv = capability.NullCap \<longrightarrow> P cap\<rbrace>
 2. \<And>srcCTE. \<lbrace>?P'111 srcCTE\<rbrace> getCTE dest \<lbrace>\<lambda>rv s. p \<noteq> dest \<longrightarrow> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap \<longrightarrow> (p = src \<longrightarrow> mdbPrev (cteMDBNode rv) = nullPointer \<and> mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> cteCap rv = capability.NullCap \<longrightarrow> P (capFreeIndex_update (\<lambda>_. maxFreeIndex (capBlockSize cap)) (cteCap srcCTE))) \<and> (p \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode rv) = nullPointer \<and> mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> cteCap rv = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> (\<not> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode rv) = nullPointer \<and> mdbNext (cteMDBNode rv) = nullPointer \<longrightarrow> cteCap rv = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)\<rbrace>
 3. \<lbrace>?Q6\<rbrace> getCTE src \<lbrace>\<lambda>srcCTE s. (p = dest \<longrightarrow> ?P'112 srcCTE s) \<and> ?P'111 srcCTE s\<rbrace>
 4. \<And>s. if p = dest then P cap else p \<noteq> src \<and> cte_wp_at' (\<lambda>c. P (cteCap c)) p s \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. if p = dest then P cap else p \<noteq> src \<and> cte_wp_at' (\<lambda>c. P (cteCap c)) p s \<Longrightarrow> \<forall>cte. ctes_of s src = Some cte \<longrightarrow> (p = dest \<longrightarrow> (\<forall>cte. ctes_of s dest = Some cte \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> cteCap cte = capability.NullCap \<longrightarrow> P cap)) \<and> (\<forall>ctea. ctes_of s dest = Some ctea \<longrightarrow> p \<noteq> dest \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (p = src \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> P (capFreeIndex_update (\<lambda>_. maxFreeIndex (capBlockSize cap)) (cteCap cte))) \<and> (p \<noteq> src \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) \<and> (\<not> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap) \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) proof (prove)
goal:
No subgoals!