theory CSpace1_R

lemma cap_insert_objs' [wp]:
  "\<lbrace>valid_objs'
    and valid_cap' cap\<rbrace>
   cteInsert cap src dest \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" including no_pre apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def bind_assoc split del: if_split) apply (wp setCTE_valid_objs) apply simp apply wp+ apply (clarsimp simp: updateCap_def) apply (wp|simp)+ apply (rule hoare_drop_imp)+ apply wp+ apply (rule hoare_strengthen_post[OF getCTE_sp]) apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps
                 dest!: ctes_of_valid_cap'') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' cap\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' cap\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' cap\<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>rv. valid_objs'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>srcCTE x y ya yb. \<lbrace>?P'20 srcCTE x y ya yb\<rbrace> getCTE dest \<lbrace>\<lambda>rv. valid_cap' (cteCap (cteCap_update (\<lambda>_. cap) rv))\<rbrace>
 2. \<And>srcCTE x y ya. \<lbrace>?B9 srcCTE x y ya\<rbrace> 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 () \<lbrace>\<lambda>yb s. valid_objs' s \<and> ?P'20 srcCTE x y ya yb s\<rbrace>
 3. \<And>srcCTE x y. \<lbrace>?B8 srcCTE x y\<rbrace> assert (mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B9 srcCTE x y\<rbrace>
 4. \<And>srcCTE x. \<lbrace>?B7 srcCTE x\<rbrace> assert (cteCap x = capability.NullCap) \<lbrace>?B8 srcCTE x\<rbrace>
 5. \<And>srcCTE. \<lbrace>?B6 srcCTE\<rbrace> getCTE dest \<lbrace>?B7 srcCTE\<rbrace>
 6. \<lbrace>valid_objs' and valid_cap' cap\<rbrace> getCTE src \<lbrace>?B6\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>srcCTE x. \<lbrace>?P'20 srcCTE x () () ()\<rbrace> getCTE dest \<lbrace>\<lambda>rv. valid_cap' cap\<rbrace>
 2. \<And>srcCTE x y ya. \<lbrace>?B9 srcCTE x y ya\<rbrace> 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 () \<lbrace>\<lambda>yb s. valid_objs' s \<and> ?P'20 srcCTE x y ya yb s\<rbrace>
 3. \<And>srcCTE x y. \<lbrace>?B8 srcCTE x y\<rbrace> assert (mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B9 srcCTE x y\<rbrace>
 4. \<And>srcCTE x. \<lbrace>?B7 srcCTE x\<rbrace> assert (cteCap x = capability.NullCap) \<lbrace>?B8 srcCTE x\<rbrace>
 5. \<And>srcCTE. \<lbrace>?B6 srcCTE\<rbrace> getCTE dest \<lbrace>?B7 srcCTE\<rbrace>
 6. \<lbrace>valid_objs' and valid_cap' cap\<rbrace> getCTE src \<lbrace>?B6\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>srcCTE x y ya. isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap \<Longrightarrow> \<lbrace>?P'32 srcCTE x y ya\<rbrace> getCTE src \<lbrace>\<lambda>rv s. valid_cap' (cteCap (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. maxFreeIndex (capBlockSize cap)) (cteCap srcCTE)) rv)) s \<and> valid_cap' cap s\<rbrace>
 2. \<And>srcCTE x y ya. \<not> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap) \<Longrightarrow> \<lbrace>?R26 srcCTE x y ya\<rbrace> return () \<lbrace>\<lambda>yb s. valid_objs' s \<and> valid_cap' cap s\<rbrace>
 3. \<And>srcCTE x y. \<lbrace>?B8 srcCTE x y\<rbrace> assert (mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>\<lambda>ya s. (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap \<longrightarrow> valid_objs' s \<and> ?P'32 srcCTE x y ya s) \<and> (\<not> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap) \<longrightarrow> ?R26 srcCTE x y ya s)\<rbrace>
 4. \<And>srcCTE x. \<lbrace>?B7 srcCTE x\<rbrace> assert (cteCap x = capability.NullCap) \<lbrace>?B8 srcCTE x\<rbrace>
 5. \<And>srcCTE. \<lbrace>?B6 srcCTE\<rbrace> getCTE dest \<lbrace>?B7 srcCTE\<rbrace>
 6. \<lbrace>valid_objs' and valid_cap' cap\<rbrace> getCTE src \<lbrace>?B6\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>srcCTE x. \<lbrakk>isUntypedCap (cteCap srcCTE); isUntypedCap cap; capPtr (cteCap srcCTE) = capPtr cap; capBlockSize (cteCap srcCTE) = capBlockSize cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'32 srcCTE x () ()\<rbrace> getCTE src \<lbrace>\<lambda>rv s. valid_cap' (capFreeIndex_update (\<lambda>_. maxFreeIndex (capBlockSize cap)) (cteCap srcCTE)) s \<and> valid_cap' cap s\<rbrace>
 2. \<And>srcCTE x y ya. \<not> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap) \<Longrightarrow> \<lbrace>?R26 srcCTE x y ya\<rbrace> return () \<lbrace>\<lambda>yb s. valid_objs' s \<and> valid_cap' cap s\<rbrace>
 3. \<And>srcCTE x y. \<lbrace>?B8 srcCTE x y\<rbrace> assert (mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>\<lambda>ya s. (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap \<longrightarrow> valid_objs' s \<and> ?P'32 srcCTE x y ya s) \<and> (\<not> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap) \<longrightarrow> ?R26 srcCTE x y ya s)\<rbrace>
 4. \<And>srcCTE x. \<lbrace>?B7 srcCTE x\<rbrace> assert (cteCap x = capability.NullCap) \<lbrace>?B8 srcCTE x\<rbrace>
 5. \<And>srcCTE. \<lbrace>?B6 srcCTE\<rbrace> getCTE dest \<lbrace>?B7 srcCTE\<rbrace>
 6. \<lbrace>valid_objs' and valid_cap' cap\<rbrace> getCTE src \<lbrace>?B6\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>srcCTE. \<lbrace>?B6 srcCTE\<rbrace> getCTE dest \<lbrace>\<lambda>x s. cteCap x = capability.NullCap \<longrightarrow> mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer \<longrightarrow> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap \<longrightarrow> valid_objs' s \<and> valid_cap' (capFreeIndex_update (\<lambda>_. maxFreeIndex (capBlockSize cap)) (cteCap srcCTE)) s \<and> valid_cap' cap s) \<and> ((capPtr (cteCap srcCTE) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize cap) \<longrightarrow> valid_objs' s \<and> valid_cap' cap s)\<rbrace>
 2. \<lbrace>valid_objs' and valid_cap' cap\<rbrace> getCTE src \<lbrace>?B6\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>srcCTE. \<lbrace>?B6 srcCTE\<rbrace> getCTE dest \<lbrace>\<lambda>rv s. (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap \<longrightarrow> valid_objs' s \<and> valid_cap' (capFreeIndex_update (\<lambda>_. maxFreeIndex (capBlockSize cap)) (cteCap srcCTE)) s \<and> valid_cap' cap s) \<and> ((capPtr (cteCap srcCTE) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize cap) \<longrightarrow> valid_objs' s \<and> valid_cap' cap s)\<rbrace>
 2. \<lbrace>valid_objs' and valid_cap' cap\<rbrace> getCTE src \<lbrace>?B6\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' cap\<rbrace> getCTE src \<lbrace>\<lambda>srcCTE s. (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap \<longrightarrow> valid_objs' s \<and> valid_cap' (capFreeIndex_update (\<lambda>_. maxFreeIndex (capBlockSize cap)) (cteCap srcCTE)) s \<and> valid_cap' cap s) \<and> ((capPtr (cteCap srcCTE) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize cap) \<longrightarrow> valid_objs' s \<and> valid_cap' cap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (cte_wp_at' (\<lambda>c. c = rv) src and (valid_objs' and valid_cap' cap)) s \<Longrightarrow> (isUntypedCap (cteCap rv) \<and> isUntypedCap cap \<and> capPtr (cteCap rv) = capPtr cap \<and> capBlockSize (cteCap rv) = capBlockSize cap \<longrightarrow> valid_objs' s \<and> valid_cap' (capFreeIndex_update (\<lambda>_. maxFreeIndex (capBlockSize cap)) (cteCap rv)) s \<and> valid_cap' cap s) \<and> ((capPtr (cteCap rv) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap rv) \<longrightarrow> capBlockSize (cteCap rv) \<noteq> capBlockSize cap) \<longrightarrow> valid_objs' s \<and> valid_cap' cap s) proof (prove)
goal:
No subgoals!