theory PageTableDuplicates

lemma resetUntypedCap_valid_duplicates'[wp]:
  "\<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s))
      and valid_objs' and cte_wp_at' (isUntypedCap o cteCap) slot\<rbrace>
    resetUntypedCap slot
  \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>"
  (is "\<lbrace>?P\<rbrace> ?f \<lbrace>\<lambda>_. ?Q\<rbrace>") apply (clarsimp simp: resetUntypedCap_def) apply (rule hoare_pre) apply (wp | simp add: unless_def)+ apply (wp mapME_x_inv_wp preemptionPoint_inv | simp | wp (once) hoare_drop_imps)+ apply (wp getSlotCap_wp) apply (clarsimp simp: cte_wp_at_ctes_of split del: if_split) apply (frule cte_wp_at_valid_objs_valid_cap'[OF ctes_of_cte_wpD], clarsimp+) apply (clarsimp simp add: isCap_simps valid_cap_simps' capAligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_objs' and cte_wp_at' (isUntypedCap \<circ> cteCap) slot\<rbrace> resetUntypedCap slot \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_objs' 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>r s. vs_valid_duplicates' (ksPSpace s)\<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>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>s. ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_objs' and cte_wp_at' (isUntypedCap \<circ> cteCap) slot) s \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrakk>0 < capFreeIndex cap; \<not> capIsDevice cap \<and> \<not> capBlockSize cap < resetChunkBits\<rbrakk> \<Longrightarrow> \<lbrace>?R12 cap ()\<rbrace> 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]) \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>cap. capFreeIndex cap \<noteq> 0 \<Longrightarrow> \<lbrace>?Q10 cap\<rbrace> liftE (deleteObjects (capPtr cap) (capBlockSize cap)) \<lbrace>\<lambda>y s. (capIsDevice cap \<or> capBlockSize cap < resetChunkBits \<longrightarrow> (if capIsDevice cap then \<lambda>s. vs_valid_duplicates' (ksPSpace s) else (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s) \<and> (\<not> (capIsDevice cap \<or> capBlockSize cap < resetChunkBits) \<longrightarrow> ?R12 cap y s)\<rbrace>, \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<lbrace>?Q4\<rbrace> liftE (getSlotCap slot) \<lbrace>\<lambda>cap. if capFreeIndex cap = 0 then \<lambda>s. vs_valid_duplicates' (ksPSpace s) else ?Q10 cap\<rbrace>, \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>s. ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_objs' and cte_wp_at' (isUntypedCap \<circ> cteCap) slot) s \<Longrightarrow> ?Q4 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> getSlotCap slot \<lbrace>\<lambda>cap. if capFreeIndex cap = 0 then \<lambda>s. vs_valid_duplicates' (ksPSpace s) else (\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<and> is_aligned (capPtr cap) (capBlockSize cap))\<rbrace>
 2. \<And>s. ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_objs' and cte_wp_at' (isUntypedCap \<circ> cteCap) slot) s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_objs' 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 \<lambda>s. vs_valid_duplicates' (ksPSpace s) else (\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<and> is_aligned (capPtr cap) (capBlockSize cap))) s proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>vs_valid_duplicates' (ksPSpace s); valid_objs' s; ctes_of s slot = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> (if capFreeIndex (cteCap cte) = 0 then \<lambda>s. vs_valid_duplicates' (ksPSpace s) else (\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<and> is_aligned (capPtr (cteCap cte)) (capBlockSize (cteCap cte)))) s proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>vs_valid_duplicates' (ksPSpace s); valid_objs' s; ctes_of s slot = Some cte; isUntypedCap (cteCap cte); valid_cap' (cteCap cte) s; 0 < capFreeIndex (cteCap cte)\<rbrakk> \<Longrightarrow> is_aligned (capPtr (cteCap cte)) (capBlockSize (cteCap cte)) proof (prove)
goal:
No subgoals!