theory Detype_R

lemma deleteObjects_invs':
  "\<lbrace>cte_wp_at' (\<lambda>c. cteCap c = UntypedCap d ptr bits idx) p
     and invs' and ct_active' and sch_act_simple
     and (\<lambda>s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s))
     and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace>
     deleteObjects ptr bits
   \<lbrace>\<lambda>rv. invs'\<rbrace>" proof - show ?thesis apply (rule hoare_pre) apply (rule_tac G="is_aligned ptr bits \<and> 2 \<le> bits \<and> bits \<le> word_bits" in hoare_grab_asm) apply (clarsimp simp add: deleteObjects_def2) apply (simp add: freeMemory_def bind_assoc doMachineOp_bind ef_storeWord) apply (simp add: bind_assoc[where f="\<lambda>_. modify f" for f, symmetric]) apply (simp add: mapM_x_storeWord_step[simplified word_size_bits_def]
                    doMachineOp_modify modify_modify) apply (simp add: bind_assoc intvl_range_conv'[where 'a=32, folded word_bits_def] mask_def field_simps) apply (wp) apply (simp cong: if_cong) apply (subgoal_tac "is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits",simp) apply clarsimp apply (frule(2) delete_locale.intro, simp_all)[1] apply (rule subst[rotated, where P=invs'], erule delete_locale.delete_invs') apply (simp add: field_simps) apply clarsimp apply (drule invs_valid_objs') apply (drule (1) cte_wp_at_valid_objs_valid_cap') apply (clarsimp simp add: valid_cap'_def capAligned_def minUntypedSizeBits_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace> deleteObjects ptr bits \<lbrace>\<lambda>rv. invs'\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace> deleteObjects ptr bits \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace> deleteObjects ptr bits \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> deleteObjects ptr bits \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>s. (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \<and> is_aligned ptr bits)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. is_aligned ptr bits \<and> 2 \<le> bits \<and> bits \<le> word_bits \<Longrightarrow> \<lbrace>?P3\<rbrace> deleteObjects ptr bits \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>s. (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \<and> is_aligned ptr bits)) s \<Longrightarrow> (is_aligned ptr bits \<and> 2 \<le> bits \<and> bits \<le> word_bits) \<and> ?P3 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits \<le> word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?P3\<rbrace> do y <- stateAssert (deletionIsSafe ptr bits) [];
y <- doMachineOp (freeMemory ptr bits);
y <- stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1)) [];
y <- modify (\<lambda>s. s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>);
stateAssert ksASIDMapSafe []
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>s. (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \<and> is_aligned ptr bits)) s \<Longrightarrow> (is_aligned ptr bits \<and> 2 \<le> bits \<and> bits \<le> word_bits) \<and> ?P3 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits \<le> word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?P3\<rbrace> do y <- stateAssert (deletionIsSafe ptr bits) [];
y <- doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1]);
y <- stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1)) [];
y <- modify (\<lambda>s. s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>);
stateAssert ksASIDMapSafe []
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>s. (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \<and> is_aligned ptr bits)) s \<Longrightarrow> (is_aligned ptr bits \<and> 2 \<le> bits \<and> bits \<le> word_bits) \<and> ?P3 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits \<le> word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?P3\<rbrace> do y <- stateAssert (deletionIsSafe ptr bits) [];
y <- doMachineOp (mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ bits - 1]);
y <- do _ <- stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1)) [];
modify (\<lambda>s. s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>)
od;
stateAssert ksASIDMapSafe []
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>s. (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \<and> is_aligned ptr bits)) s \<Longrightarrow> (is_aligned ptr bits \<and> 2 \<le> bits \<and> bits \<le> word_bits) \<and> ?P3 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits \<le> word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?P3\<rbrace> do y <- stateAssert (deletionIsSafe ptr bits) [];
y <- modify (ksMachineState_update (underlying_memory_update (\<lambda>m x. if \<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits then 0 else m x)));
y <- do _ <- stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1)) [];
modify (\<lambda>s. s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>)
od;
stateAssert ksASIDMapSafe []
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>s. (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \<and> is_aligned ptr bits)) s \<Longrightarrow> (is_aligned ptr bits \<and> 2 \<le> bits \<and> bits \<le> word_bits) \<and> ?P3 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr bits; 2 \<le> bits; bits \<le> word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?P3\<rbrace> do y <- stateAssert (deletionIsSafe ptr bits) [];
y <- modify (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)));
x <- stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1)) [];
y <- modify (\<lambda>s. s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>);
stateAssert ksASIDMapSafe []
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>s. (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \<and> is_aligned ptr bits)) s \<Longrightarrow> (is_aligned ptr bits \<and> 2 \<le> bits \<and> bits \<le> word_bits) \<and> ?P3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \<and> is_aligned ptr bits)) s \<Longrightarrow> (is_aligned ptr bits \<and> 2 \<le> bits \<and> bits \<le> word_bits) \<and> (deletionIsSafe ptr bits s \<longrightarrow> \<not> cNodePartialOverlap (gsCNodes (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s)) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1) \<longrightarrow> ksASIDMapSafe (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s) x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s) x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s) x\<rparr>) \<longrightarrow> invs' (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s) x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s) x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s) x\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p s \<and> invs' s \<and> ct_active' s \<and> sch_act_simple s \<and> descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s) \<and> bits < word_bits \<and> is_aligned ptr bits \<Longrightarrow> 2 \<le> bits \<and> (deletionIsSafe ptr bits s \<longrightarrow> \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1) \<longrightarrow> ksASIDMapSafe (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>) \<longrightarrow> invs' (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p s \<and> invs' s \<and> ct_active' s \<and> sch_act_simple s \<and> descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s); is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits\<rbrakk> \<Longrightarrow> deletionIsSafe ptr bits s \<longrightarrow> \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1) \<longrightarrow> ksASIDMapSafe (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>) \<longrightarrow> invs' (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x\<rparr>)
 2. \<And>s. cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p s \<and> invs' s \<and> ct_active' s \<and> sch_act_simple s \<and> descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s) \<and> bits < word_bits \<and> is_aligned ptr bits \<Longrightarrow> is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p s; is_aligned ptr bits; invs' s; 2 \<le> bits; bits < word_bits; ct_active' s; sch_act_simple s; descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s); deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ksASIDMapSafe (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>)\<rbrakk> \<Longrightarrow> invs' (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x\<rparr>)
 2. \<And>s. cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p s \<and> invs' s \<and> ct_active' s \<and> sch_act_simple s \<and> descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s) \<and> bits < word_bits \<and> is_aligned ptr bits \<Longrightarrow> is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p s; is_aligned ptr bits; invs' s; 2 \<le> bits; bits < word_bits; ct_active' s; sch_act_simple s; descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s); deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ksASIDMapSafe (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>); delete_locale s ptr bits p idx d\<rbrakk> \<Longrightarrow> invs' (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x\<rparr>)
 2. \<And>s. cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p s \<and> invs' s \<and> ct_active' s \<and> sch_act_simple s \<and> descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s) \<and> bits < word_bits \<and> is_aligned ptr bits \<Longrightarrow> is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p s; is_aligned ptr bits; invs' s; 2 \<le> bits; bits < word_bits; ct_active' s; sch_act_simple s; descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s); deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ksASIDMapSafe (ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>); delete_locale s ptr bits p idx d\<rbrakk> \<Longrightarrow> ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + (2 ^ bits - 1) then 0 else m x)) (s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + (2 ^ bits - 1) then None else ksPSpace s x\<rparr>) = ksMachineState_update (underlying_memory_update (\<lambda>m x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else m x)) s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x\<rparr>
 2. \<And>s. cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p s \<and> invs' s \<and> ct_active' s \<and> sch_act_simple s \<and> descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s) \<and> bits < word_bits \<and> is_aligned ptr bits \<Longrightarrow> is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p s \<and> invs' s \<and> ct_active' s \<and> sch_act_simple s \<and> descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s) \<and> bits < word_bits \<and> is_aligned ptr bits \<Longrightarrow> is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p s; invs' s; ct_active' s; sch_act_simple s; descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s); bits < word_bits; is_aligned ptr bits\<rbrakk> \<Longrightarrow> 2 \<le> bits proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p s; ct_active' s; sch_act_simple s; descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s); bits < word_bits; is_aligned ptr bits; valid_objs' s\<rbrakk> \<Longrightarrow> 2 \<le> bits proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ct_active' s; sch_act_simple s; descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s); bits < word_bits; is_aligned ptr bits; valid_objs' s; \<exists>cte. cteCap cte = capability.UntypedCap d ptr bits idx \<and> valid_cap' (cteCap cte) s\<rbrakk> \<Longrightarrow> 2 \<le> bits proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace> deleteObjects ptr bits \<lbrace>\<lambda>rv. invs'\<rbrace>

goal:
No subgoals!