theory Detype_R

lemma deleteObjects_cap_to':
  "\<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 ex_cte_cap_to' p'
     and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace>
      deleteObjects ptr bits
   \<lbrace>\<lambda>rv. ex_cte_cap_to' p'\<rbrace>" apply (simp add: deleteObjects_def3 doMachineOp_def split_def) apply wp apply clarsimp apply (subgoal_tac "delete_locale s ptr bits p idx d") apply (drule delete_locale.delete_ex_cte_cap_to', assumption) apply (simp cong:if_cong) apply (subgoal_tac
     "s\<lparr>ksMachineState := b,
        ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None
                        else ksPSpace s x\<rparr> =
      ksMachineState_update (\<lambda>_. b)
      (s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None
                         else ksPSpace s x\<rparr>)",erule ssubst) apply (simp add: field_simps ex_cte_cap_wp_to'_def cong:if_cong) apply simp apply (simp add: delete_locale_def) done

(* 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 ex_cte_cap_wp_to' (\<lambda>_. True) p' and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace> deleteObjects ptr bits \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' (\<lambda>_. True) p'\<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 ex_cte_cap_wp_to' (\<lambda>_. True) p' and (\<lambda>y. bits < word_bits \<and> is_aligned ptr bits)\<rbrace> do y <- assert (is_aligned ptr bits);
y <- stateAssert (deletionIsSafe ptr bits) [];
y <- do ms <- gets ksMachineState;
p <- select_f (freeMemory ptr bits ms);
modify (ksMachineState_update (\<lambda>_. snd p))
od;
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. ex_cte_cap_wp_to' (\<lambda>_. True) p'\<rbrace> 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 ex_cte_cap_wp_to' (\<lambda>_. True) p' and (\<lambda>y. bits < word_bits \<and> is_aligned ptr bits)) s \<Longrightarrow> is_aligned ptr bits \<longrightarrow> deletionIsSafe ptr bits s \<longrightarrow> (\<forall>x\<in>fst (freeMemory ptr bits (ksMachineState s)). \<not> cNodePartialOverlap (gsCNodes (s\<lparr>ksMachineState := snd x\<rparr>)) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1) \<longrightarrow> ksASIDMapSafe (s\<lparr>ksMachineState := snd x, ksPSpace := \<lambda>xa. if ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (s\<lparr>ksMachineState := snd x\<rparr>) xa, gsUserPages := \<lambda>xa. if ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 then None else gsUserPages (s\<lparr>ksMachineState := snd x\<rparr>) xa, gsCNodes := \<lambda>xa. if ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 then None else gsCNodes (s\<lparr>ksMachineState := snd x\<rparr>) xa\<rparr>) \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) p' (s\<lparr>ksMachineState := snd x, ksPSpace := \<lambda>xa. if ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (s\<lparr>ksMachineState := snd x\<rparr>) xa, gsUserPages := \<lambda>xa. if ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 then None else gsUserPages (s\<lparr>ksMachineState := snd x\<rparr>) xa, gsCNodes := \<lambda>xa. if ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 then None else gsCNodes (s\<lparr>ksMachineState := snd x\<rparr>) xa\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<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); ex_cte_cap_wp_to' (\<lambda>_. True) p' s; bits < word_bits; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x\<rparr>)\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) p' (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<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); ex_cte_cap_wp_to' (\<lambda>_. True) p' s; bits < word_bits; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x\<rparr>); delete_locale s ptr bits p idx d\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) p' (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x\<rparr>)
 2. \<And>s b. \<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); ex_cte_cap_wp_to' (\<lambda>_. True) p' s; bits < word_bits; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x\<rparr>)\<rbrakk> \<Longrightarrow> delete_locale s ptr bits p idx d proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<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); ex_cte_cap_wp_to' (\<lambda>_. True) p' s; bits < word_bits; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x\<rparr>); ex_cte_cap_wp_to' (\<lambda>_. True) p' (s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + (2 ^ bits - 1) then None else ksPSpace s x\<rparr>)\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) p' (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x\<rparr>)
 2. \<And>s b. \<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); ex_cte_cap_wp_to' (\<lambda>_. True) p' s; bits < word_bits; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x\<rparr>)\<rbrakk> \<Longrightarrow> delete_locale s ptr bits p idx d proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<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); ex_cte_cap_wp_to' (\<lambda>_. True) p' s; bits < word_bits; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, 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>); ex_cte_cap_wp_to' (\<lambda>_. True) p' (s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + (2 ^ bits - 1) then None else ksPSpace s x\<rparr>)\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) p' (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x\<rparr>)
 2. \<And>s b. \<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); ex_cte_cap_wp_to' (\<lambda>_. True) p' s; bits < word_bits; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x\<rparr>)\<rbrakk> \<Longrightarrow> delete_locale s ptr bits p idx d proof (prove)
goal (3 subgoals):
 1. \<And>s b. \<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); ex_cte_cap_wp_to' (\<lambda>_. True) p' s; bits < word_bits; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, 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>); ex_cte_cap_wp_to' (\<lambda>_. True) p' (s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + (2 ^ bits - 1) then None else ksPSpace s x\<rparr>)\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) p' (s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, ksMachineState := b\<rparr>)
 2. \<And>s b. \<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); ex_cte_cap_wp_to' (\<lambda>_. True) p' s; bits < word_bits; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, 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>); ex_cte_cap_wp_to' (\<lambda>_. True) p' (s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + (2 ^ bits - 1) then None else ksPSpace s x\<rparr>)\<rbrakk> \<Longrightarrow> s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x\<rparr> = s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, ksMachineState := b\<rparr>
 3. \<And>s b. \<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); ex_cte_cap_wp_to' (\<lambda>_. True) p' s; bits < word_bits; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x\<rparr>)\<rbrakk> \<Longrightarrow> delete_locale s ptr bits p idx d proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<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); ex_cte_cap_wp_to' (\<lambda>_. True) p' s; bits < word_bits; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, 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>); ex_cte_cap_wp_to' (\<lambda>_. True) p' (s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + (2 ^ bits - 1) then None else ksPSpace s x\<rparr>)\<rbrakk> \<Longrightarrow> s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x\<rparr> = s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, ksMachineState := b\<rparr>
 2. \<And>s b. \<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); ex_cte_cap_wp_to' (\<lambda>_. True) p' s; bits < word_bits; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x\<rparr>)\<rbrakk> \<Longrightarrow> delete_locale s ptr bits p idx d proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<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); ex_cte_cap_wp_to' (\<lambda>_. True) p' s; bits < word_bits; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes (s\<lparr>ksMachineState := snd ((), b)\<rparr>) x\<rparr>)\<rbrakk> \<Longrightarrow> delete_locale s ptr bits p idx d proof (prove)
goal:
No subgoals!