theory Untyped_R

lemma deleteObjects_ex_cte_cap_wp_to':
  "\<lbrace>invs' and ex_cte_cap_wp_to' P slot and (\<lambda>s. descendants_of' p (ctes_of s) = {})
      and cte_wp_at' (\<lambda>cte. \<exists>idx d. cteCap cte = UntypedCap d ptr sz idx) p\<rbrace>
    deleteObjects ptr sz
  \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P slot\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp: cte_wp_at_ctes_of) apply (rule hoare_pre) apply (simp add: ex_cte_cap_wp_to'_def) apply wps apply (wp hoare_vcg_ex_lift) apply (rule_tac idx=idx in deleteObjects_cte_wp_at') apply (clarsimp simp: cte_wp_at_ctes_of) apply (frule ctes_of_valid[OF ctes_of_cte_wpD], clarsimp+) apply (clarsimp simp: ex_cte_cap_wp_to'_def
                        cte_wp_at_ctes_of) apply (rule_tac x=cref in exI, simp) apply (frule_tac p=cref in if_unsafe_then_capD'[OF ctes_of_cte_wpD], clarsimp+) apply (frule descendants_range_ex_cte'[rotated, OF _ order_refl, where p=p],
    (simp add: isCap_simps empty_descendants_range_in')+) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ex_cte_cap_wp_to' P slot and (\<lambda>s. descendants_of' p (ctes_of s) = {}) and cte_wp_at' (\<lambda>cte. \<exists>idx d. cteCap cte = capability.UntypedCap d ptr sz idx) p\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and ex_cte_cap_wp_to' P slot and (\<lambda>s. descendants_of' p (ctes_of s) = {}) and cte_wp_at' (\<lambda>cte. \<exists>idx d. cteCap cte = capability.UntypedCap d ptr sz idx) p) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s cte idx d. \<lbrakk>invs' s; ex_cte_cap_wp_to' P slot s; descendants_of' p (ctes_of s) = {}; ctes_of s p = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s cte idx d. \<lbrakk>invs' s; ex_cte_cap_wp_to' P slot s; descendants_of' p (ctes_of s) = {}; ctes_of s p = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 s cte idx d\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P slot\<rbrace>
 2. \<And>s cte idx d sa. \<lbrakk>invs' s; ex_cte_cap_wp_to' P slot s; descendants_of' p (ctes_of s) = {}; ctes_of s p = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx; s = sa\<rbrakk> \<Longrightarrow> ?Q9 s cte idx d sa proof (prove)
goal (2 subgoals):
 1. \<And>s cte idx d. \<lbrakk>invs' s; \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> slot \<in> cte_refs' (cteCap c) (irq_node' s)) cref s; descendants_of' p (ctes_of s) = {}; ctes_of s p = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 s cte idx d\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> slot \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrace>
 2. \<And>s cte idx d sa. \<lbrakk>invs' s; ex_cte_cap_wp_to' P slot s; descendants_of' p (ctes_of s) = {}; ctes_of s p = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx; s = sa\<rbrakk> \<Longrightarrow> ?Q9 s cte idx d sa proof (prove)
goal (2 subgoals):
 1. \<And>s cte idx d prev_s. \<lbrakk>invs' s; \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> slot \<in> cte_refs' (cteCap c) (irq_node' s)) cref s; descendants_of' p (ctes_of s) = {}; ctes_of s p = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx\<rbrakk> \<Longrightarrow> \<lbrace>?P12 s cte idx d prev_s\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>rv s'. \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> slot \<in> cte_refs' (cteCap c) (irq_node' prev_s)) cref s'\<rbrace>
 2. \<And>s cte idx d sa. \<lbrakk>invs' s; ex_cte_cap_wp_to' P slot s; descendants_of' p (ctes_of s) = {}; ctes_of s p = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx; s = sa\<rbrakk> \<Longrightarrow> ?P12 s cte idx d sa sa proof (prove)
goal (2 subgoals):
 1. \<And>s cte idx d prev_s cref. \<lbrakk>invs' s; \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> slot \<in> cte_refs' (cteCap c) (irq_node' s)) cref s; descendants_of' p (ctes_of s) = {}; ctes_of s p = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx\<rbrakk> \<Longrightarrow> \<lbrace>?P19 s cte idx d prev_s cref\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> slot \<in> cte_refs' (cteCap c) (irq_node' prev_s)) cref\<rbrace>
 2. \<And>s cte idx d sa. \<lbrakk>invs' s; ex_cte_cap_wp_to' P slot s; descendants_of' p (ctes_of s) = {}; ctes_of s p = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx; s = sa\<rbrakk> \<Longrightarrow> \<exists>x. ?P19 s cte idx d sa x sa proof (prove)
goal (1 subgoal):
 1. \<And>s cte idx d sa. \<lbrakk>invs' s; ex_cte_cap_wp_to' P slot s; descendants_of' p (ctes_of s) = {}; ctes_of s p = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx; s = sa\<rbrakk> \<Longrightarrow> \<exists>x. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> slot \<in> cte_refs' (cteCap c) (irq_node' sa)) x sa \<and> x \<notin> {ptr..ptr + 2 ^ sz - 1} \<and> valid_cap' (capability.UntypedCap (?d21 s cte idx d sa x) ptr sz idx) sa \<and> valid_pspace' sa proof (prove)
goal (1 subgoal):
 1. \<And>cte idx d sa. \<lbrakk>invs' sa; ex_cte_cap_wp_to' P slot sa; descendants_of' p (ctes_of sa) = {}; ctes_of sa p = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>cte. ctes_of sa x = Some cte \<and> P (cteCap cte) \<and> slot \<in> cte_refs' (cteCap cte) (irq_node' sa)) \<and> (ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ sz - 1) \<and> valid_cap' (capability.UntypedCap (?d21 sa cte idx d sa x) ptr sz idx) sa \<and> valid_pspace' sa proof (prove)
goal (1 subgoal):
 1. \<And>cte idx d sa. \<lbrakk>invs' sa; ex_cte_cap_wp_to' P slot sa; descendants_of' p (ctes_of sa) = {}; ctes_of sa p = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx; valid_cap' (capability.UntypedCap d ptr sz idx) sa\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>cte. ctes_of sa x = Some cte \<and> P (cteCap cte) \<and> slot \<in> cte_refs' (cteCap cte) (irq_node' sa)) \<and> (ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ sz - 1) \<and> valid_cap' (capability.UntypedCap (?d21 sa cte idx d sa x) ptr sz idx) sa \<and> valid_pspace' sa proof (prove)
goal (1 subgoal):
 1. \<And>cte idx d sa cref ctea. \<lbrakk>invs' sa; descendants_of' p (ctes_of sa) = {}; ctes_of sa p = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx; valid_cap' (capability.UntypedCap d ptr sz idx) sa; ctes_of sa cref = Some ctea; P (cteCap ctea); slot \<in> cte_refs' (cteCap ctea) (irq_node' sa)\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>cte. ctes_of sa x = Some cte \<and> P (cteCap cte) \<and> slot \<in> cte_refs' (cteCap cte) (irq_node' sa)) \<and> (ptr \<le> x \<longrightarrow> \<not> x \<le> ptr + 2 ^ sz - 1) \<and> valid_cap' (capability.UntypedCap (?d21 sa cte idx d sa x) ptr sz idx) sa \<and> valid_pspace' sa proof (prove)
goal (1 subgoal):
 1. \<And>cte idx d sa cref ctea. \<lbrakk>invs' sa; descendants_of' p (ctes_of sa) = {}; ctes_of sa p = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx; valid_cap' (capability.UntypedCap d ptr sz idx) sa; ctes_of sa cref = Some ctea; P (cteCap ctea); slot \<in> cte_refs' (cteCap ctea) (irq_node' sa)\<rbrakk> \<Longrightarrow> (ptr \<le> cref \<longrightarrow> \<not> cref \<le> ptr + 2 ^ sz - 1) \<and> valid_cap' (capability.UntypedCap (?d21 sa cte idx d sa cref) ptr sz idx) sa \<and> valid_pspace' sa proof (prove)
goal (1 subgoal):
 1. \<And>cte idx d sa cref ctea. \<lbrakk>invs' sa; descendants_of' p (ctes_of sa) = {}; ctes_of sa p = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx; valid_cap' (capability.UntypedCap d ptr sz idx) sa; ctes_of sa cref = Some ctea; P (cteCap ctea); slot \<in> cte_refs' (cteCap ctea) (irq_node' sa); ex_cte_cap_wp_to' (\<lambda>_. True) cref sa\<rbrakk> \<Longrightarrow> (ptr \<le> cref \<longrightarrow> \<not> cref \<le> ptr + 2 ^ sz - 1) \<and> valid_cap' (capability.UntypedCap (?d21 sa cte idx d sa cref) ptr sz idx) sa \<and> valid_pspace' sa proof (prove)
goal (1 subgoal):
 1. \<And>cte idx d sa cref ctea. \<lbrakk>invs' sa; descendants_of' p (ctes_of sa) = {}; ctes_of sa p = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx; valid_cap' (capability.UntypedCap d ptr sz idx) sa; ctes_of sa cref = Some ctea; P (cteCap ctea); slot \<in> cte_refs' (cteCap ctea) (irq_node' sa); ex_cte_cap_wp_to' (\<lambda>_. True) cref sa; ptr \<le> cref \<longrightarrow> \<not> cref \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> valid_cap' (capability.UntypedCap (?d21 sa cte idx d sa cref) ptr sz idx) sa \<and> valid_pspace' sa proof (prove)
goal:
No subgoals!