theory Orphanage

lemma resetUntypedCap_no_orphans [wp]:
  "\<lbrace> (\<lambda>s. no_orphans s \<and> pspace_distinct' s \<and> valid_objs' s)
      and cte_wp_at' (isUntypedCap o cteCap) slot\<rbrace>
    resetUntypedCap slot
  \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" apply (simp add: resetUntypedCap_def) apply (rule hoare_pre) apply (wp mapME_x_inv_wp preemptionPoint_inv getSlotCap_wp hoare_drop_imps
     | simp add: unless_def split del: if_split)+ apply (clarsimp simp: cte_wp_at_ctes_of split del: if_split) apply (frule(1) cte_wp_at_valid_objs_valid_cap'[OF ctes_of_cte_wpD]) apply (clarsimp simp: isCap_simps valid_cap_simps' capAligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_distinct' s \<and> valid_objs' s) and cte_wp_at' (isUntypedCap \<circ> cteCap) slot\<rbrace> resetUntypedCap slot \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_distinct' s \<and> valid_objs' s) and cte_wp_at' (isUntypedCap \<circ> cteCap) slot\<rbrace> doE cap <- liftE (getSlotCap slot);
unlessE (capFreeIndex cap = 0) (doE y <- liftE (deleteObjects (capPtr cap) (capBlockSize cap));
if capIsDevice cap \<or> capBlockSize cap < resetChunkBits then liftE (do y <- unless (capIsDevice cap) (doMachineOp (clearMemory (capPtr cap) (shiftL (Suc 0) (capBlockSize cap))));
updateFreeIndex slot 0
od) else mapME_x (\<lambda>addr. doE y <- liftE (doMachineOp (clearMemory addr (shiftL (Suc 0) resetChunkBits)));
y <- liftE (updateFreeIndex slot (getFreeIndex (capPtr cap) addr));
preemptionPoint
odE) (rev [capPtr cap , capPtr cap + 2 ^ resetChunkBits .e. getFreeRef (capPtr cap) (capFreeIndex cap) - 1])
odE)
odE \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> doE cap <- liftE (getSlotCap slot);
unlessE (capFreeIndex cap = 0) (doE y <- liftE (deleteObjects (capPtr cap) (capBlockSize cap));
if capIsDevice cap \<or> capBlockSize cap < resetChunkBits then liftE (do y <- unless (capIsDevice cap) (doMachineOp (clearMemory (capPtr cap) (shiftL (Suc 0) (capBlockSize cap))));
updateFreeIndex slot 0
od) else mapME_x (\<lambda>addr. doE y <- liftE (doMachineOp (clearMemory addr (shiftL (Suc 0) resetChunkBits)));
y <- liftE (updateFreeIndex slot (getFreeIndex (capPtr cap) addr));
preemptionPoint
odE) (rev [capPtr cap , capPtr cap + 2 ^ resetChunkBits .e. getFreeRef (capPtr cap) (capFreeIndex cap) - 1])
odE)
odE \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>s. ((\<lambda>s. no_orphans s \<and> pspace_distinct' s \<and> valid_objs' s) and cte_wp_at' (isUntypedCap \<circ> cteCap) slot) s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. no_orphans s \<and> pspace_distinct' s \<and> valid_objs' s \<and> cte_wp_at' (isUntypedCap \<circ> cteCap) slot s \<Longrightarrow> \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> (if capFreeIndex cap = 0 then no_orphans else (\<lambda>s. no_orphans s \<and> pspace_distinct' s \<and> is_aligned (capPtr cap) (capBlockSize cap))) s proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>no_orphans s; pspace_distinct' s; valid_objs' s; ctes_of s slot = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> (if capFreeIndex (cteCap cte) = 0 then no_orphans else (\<lambda>s. no_orphans s \<and> pspace_distinct' s \<and> is_aligned (capPtr (cteCap cte)) (capBlockSize (cteCap cte)))) s proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>no_orphans s; pspace_distinct' s; valid_objs' s; ctes_of s slot = Some cte; isUntypedCap (cteCap cte); \<exists>ctea. cte = ctea \<and> valid_cap' (cteCap ctea) s\<rbrakk> \<Longrightarrow> (if capFreeIndex (cteCap cte) = 0 then no_orphans else (\<lambda>s. no_orphans s \<and> pspace_distinct' s \<and> is_aligned (capPtr (cteCap cte)) (capBlockSize (cteCap cte)))) s proof (prove)
goal:
No subgoals!