theory PageTableDuplicates

lemma deleteObjects_valid_duplicates'[wp]:
  notes blah[simp del] =  atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
          atLeastAtMost_iff
  shows
  "\<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
      K (is_aligned ptr sz)
   \<rbrace> deleteObjects ptr sz
   \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (rule hoare_gen_asm) apply (clarsimp simp:deleteObjects_def2) apply (wp hoare_drop_imps|simp)+ apply clarsimp apply (simp add:deletionIsSafe_def) apply (erule valid_duplicates_deleteObjects_helper) apply fastforce apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and K (is_aligned ptr sz)\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned ptr sz \<Longrightarrow> \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned ptr sz \<Longrightarrow> \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> do y <- stateAssert (deletionIsSafe ptr sz) [];
y <- doMachineOp (freeMemory ptr sz);
y <- stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. x \<in> {ptr..ptr + 2 ^ sz - 1})) [];
y <- modify (\<lambda>s. s\<lparr>ksPSpace := \<lambda>x. if x \<in> {ptr..ptr + 2 ^ sz - 1} then None else ksPSpace s x, gsUserPages := \<lambda>x. if x \<in> {ptr..ptr + 2 ^ sz - 1} then None else gsUserPages s x, gsCNodes := \<lambda>x. if x \<in> {ptr..ptr + 2 ^ sz - 1} then None else gsCNodes s x\<rparr>);
stateAssert ksASIDMapSafe []
od \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr sz; vs_valid_duplicates' (ksPSpace s)\<rbrakk> \<Longrightarrow> deletionIsSafe ptr sz s \<longrightarrow> vs_valid_duplicates' (\<lambda>x. if x \<in> {ptr..ptr + 2 ^ sz - 1} then None else ksPSpace s x) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr sz; vs_valid_duplicates' (ksPSpace s); deletionIsSafe ptr sz s\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (\<lambda>x. if x \<in> {ptr..ptr + 2 ^ sz - 1} then None else ksPSpace s x) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr sz; vs_valid_duplicates' (ksPSpace s); \<forall>p. (\<forall>t. (\<exists>m r. cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m r) p s) \<longrightarrow> t \<notin> {ptr..ptr + 2 ^ sz - 1}) \<and> ((\<exists>ko. ksPSpace s p = Some (KOArch ko)) \<and> p \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> 6 \<le> sz)\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (\<lambda>x. if x \<in> {ptr..ptr + 2 ^ sz - 1} then None else ksPSpace s x) proof (prove)
goal (2 subgoals):
 1. \<And>s p ko. \<lbrakk>is_aligned ptr sz; \<forall>p. (\<forall>t. (\<exists>m r. cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m r) p s) \<longrightarrow> t \<notin> {ptr..ptr + 2 ^ sz - 1}) \<and> ((\<exists>ko. ksPSpace s p = Some (KOArch ko)) \<and> p \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> 6 \<le> sz); ksPSpace s p = Some (KOArch ko); p \<in> {ptr..ptr + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> 6 \<le> sz
 2. \<And>s. \<lbrakk>is_aligned ptr sz; \<forall>p. (\<forall>t. (\<exists>m r. cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m r) p s) \<longrightarrow> t \<notin> {ptr..ptr + 2 ^ sz - 1}) \<and> ((\<exists>ko. ksPSpace s p = Some (KOArch ko)) \<and> p \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> 6 \<le> sz)\<rbrakk> \<Longrightarrow> is_aligned ptr sz proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr sz; \<forall>p. (\<forall>t. (\<exists>m r. cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m r) p s) \<longrightarrow> t \<notin> {ptr..ptr + 2 ^ sz - 1}) \<and> ((\<exists>ko. ksPSpace s p = Some (KOArch ko)) \<and> p \<in> {ptr..ptr + 2 ^ sz - 1} \<longrightarrow> 6 \<le> sz)\<rbrakk> \<Longrightarrow> is_aligned ptr sz proof (prove)
goal:
No subgoals!