theory Untyped_R

lemma deleteObjects_caps_no_overlap'':
  "\<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> sch_act_simple s \<and>
        cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr sz idx) slot s \<and>
        caps_no_overlap'' ptr sz s \<and>
        descendants_range' (capability.UntypedCap d ptr sz idx) slot (ctes_of s)\<rbrace>
   deleteObjects ptr sz
   \<lbrace>\<lambda>rv s. caps_no_overlap'' ptr sz s\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp split:if_splits) apply (clarsimp simp:caps_no_overlap''_def2 deleteObjects_def2 capAligned_def valid_cap'_def
    dest!:ctes_of_valid_cap') apply (wp deleteObjects_null_filter[where idx = idx and p = slot]) apply (clarsimp simp:cte_wp_at_ctes_of invs_def) apply (case_tac cte) apply clarsimp apply (frule ctes_of_valid_cap') apply (simp add:invs_valid_objs') apply (simp add:valid_cap'_def capAligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr sz idx) slot s \<and> caps_no_overlap'' ptr sz s \<and> descendants_range' (capability.UntypedCap d ptr sz idx) slot (ctes_of s)\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>rv. caps_no_overlap'' ptr sz\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> ct_active' s \<and> sch_act_simple s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr sz idx) slot s \<and> caps_no_overlap'' ptr sz s \<and> descendants_range' (capability.UntypedCap d ptr sz idx) slot (ctes_of s) \<Longrightarrow> \<lbrace>(=) s\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>rv. caps_no_overlap'' ptr sz\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; ct_active' s; sch_act_simple s; cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr sz idx) slot s; caps_no_overlap'' ptr sz s; descendants_range' (capability.UntypedCap d ptr sz idx) slot (ctes_of s)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>rv. caps_no_overlap'' ptr sz\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; ct_active' s; sch_act_simple s; cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr sz idx) slot s; \<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); descendants_range' (capability.UntypedCap d ptr sz idx) slot (ctes_of s)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>rv s. \<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>invs' s; ct_active' s; sch_act_simple s; cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr sz idx) slot s; \<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); descendants_range' (capability.UntypedCap d ptr sz idx) slot (ctes_of s); s = sa\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d8 s) ptr sz idx) slot and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d8 s) ptr sz idx) slot (ctes_of sa)) and (\<lambda>s. \<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)) and K (sz < word_bits \<and> is_aligned ptr sz)) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa cte. \<lbrakk>invs' sa; ct_active' sa; sch_act_simple sa; \<forall>cte\<in>ran (null_filter' (ctes_of sa)). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); descendants_range' (capability.UntypedCap d ptr sz idx) slot (ctes_of sa); ctes_of sa slot = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx\<rbrakk> \<Longrightarrow> d = ?d8 sa \<and> descendants_range' (capability.UntypedCap (?d8 sa) ptr sz idx) slot (ctes_of sa) \<and> sz < word_bits \<and> is_aligned ptr sz proof (prove)
goal (1 subgoal):
 1. \<And>sa cte x1 x2. \<lbrakk>invs' sa; ct_active' sa; sch_act_simple sa; \<forall>cte\<in>ran (null_filter' (ctes_of sa)). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); descendants_range' (capability.UntypedCap d ptr sz idx) slot (ctes_of sa); ctes_of sa slot = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> d = ?d8 sa \<and> descendants_range' (capability.UntypedCap (?d8 sa) ptr sz idx) slot (ctes_of sa) \<and> sz < word_bits \<and> is_aligned ptr sz proof (prove)
goal (1 subgoal):
 1. \<And>sa x2. \<lbrakk>invs' sa; ct_active' sa; sch_act_simple sa; \<forall>cte\<in>ran (null_filter' (ctes_of sa)). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); descendants_range' (capability.UntypedCap d ptr sz idx) slot (ctes_of sa); ctes_of sa slot = Some (CTE (capability.UntypedCap d ptr sz idx) x2)\<rbrakk> \<Longrightarrow> d = ?d8 sa \<and> descendants_range' (capability.UntypedCap (?d8 sa) ptr sz idx) slot (ctes_of sa) \<and> sz < word_bits \<and> is_aligned ptr sz proof (prove)
goal (2 subgoals):
 1. \<And>sa x2. \<lbrakk>invs' sa; ct_active' sa; sch_act_simple sa; \<forall>cte\<in>ran (null_filter' (ctes_of sa)). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); descendants_range' (capability.UntypedCap d ptr sz idx) slot (ctes_of sa); ctes_of sa slot = Some (CTE (capability.UntypedCap d ptr sz idx) x2)\<rbrakk> \<Longrightarrow> valid_objs' sa
 2. \<And>sa x2. \<lbrakk>invs' sa; ct_active' sa; sch_act_simple sa; \<forall>cte\<in>ran (null_filter' (ctes_of sa)). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); descendants_range' (capability.UntypedCap d ptr sz idx) slot (ctes_of sa); ctes_of sa slot = Some (CTE (capability.UntypedCap d ptr sz idx) x2); valid_cap' (capability.UntypedCap d ptr sz idx) sa\<rbrakk> \<Longrightarrow> d = ?d8 sa \<and> descendants_range' (capability.UntypedCap (?d8 sa) ptr sz idx) slot (ctes_of sa) \<and> sz < word_bits \<and> is_aligned ptr sz proof (prove)
goal (1 subgoal):
 1. \<And>sa x2. \<lbrakk>invs' sa; ct_active' sa; sch_act_simple sa; \<forall>cte\<in>ran (null_filter' (ctes_of sa)). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); descendants_range' (capability.UntypedCap d ptr sz idx) slot (ctes_of sa); ctes_of sa slot = Some (CTE (capability.UntypedCap d ptr sz idx) x2); valid_cap' (capability.UntypedCap d ptr sz idx) sa\<rbrakk> \<Longrightarrow> d = ?d8 sa \<and> descendants_range' (capability.UntypedCap (?d8 sa) ptr sz idx) slot (ctes_of sa) \<and> sz < word_bits \<and> is_aligned ptr sz proof (prove)
goal:
No subgoals!