theory Detype_R

lemma deleteObjects_st_tcb_at':
  "\<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 st_tcb_at' (P and (\<noteq>) Inactive and (\<noteq>) IdleThreadState) t
     and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace>
     deleteObjects ptr bits
   \<lbrace>\<lambda>rv. st_tcb_at' P t\<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_ko_wp_at'
                [where p = t and
                       P="case_option False (P \<circ> tcbState) \<circ> projectKO_opt",
                 simplified eq_commute]) apply (simp add: pred_tcb_at'_def obj_at'_real_def) apply (rule conjI) apply (fastforce elim: ko_wp_at'_weakenE) apply (erule if_live_then_nonz_capD' [rotated]) apply (clarsimp simp: projectKOs) apply (clarsimp simp: invs'_def valid_state'_def) apply (clarsimp simp: pred_tcb_at'_def obj_at'_real_def
                  field_simps ko_wp_at'_def ps_clear_def
                  cong:if_cong
                  split: option.splits) 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 st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace> deleteObjects ptr bits \<lbrace>\<lambda>rv. st_tcb_at' P t\<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 st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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. st_tcb_at' P t\<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 st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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> st_tcb_at' P t (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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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> st_tcb_at' P t (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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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> st_tcb_at' P t (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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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> ko_wp_at' (case_option False (P \<circ> tcbState) \<circ> projectKO_opt) t s \<and> ex_nonz_cap_to' t s
 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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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>); ko_wp_at' (case_option False (P \<circ> tcbState) \<circ> projectKO_opt) t (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> st_tcb_at' P t (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>)
 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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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); ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (tcbState obj) \<and> Structures_H.thread_state.Inactive \<noteq> tcbState obj \<and> Structures_H.thread_state.IdleThreadState \<noteq> tcbState obj) t 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> ko_wp_at' (case_option False (P \<circ> tcbState) \<circ> projectKO_opt) t s \<and> ex_nonz_cap_to' t s
 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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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>); ko_wp_at' (case_option False (P \<circ> tcbState) \<circ> projectKO_opt) t (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> st_tcb_at' P t (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>)
 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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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 (4 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); ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (tcbState obj) \<and> Structures_H.thread_state.Inactive \<noteq> tcbState obj \<and> Structures_H.thread_state.IdleThreadState \<noteq> tcbState obj) t 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> ko_wp_at' (case_option False (P \<circ> tcbState) \<circ> projectKO_opt) t s
 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); ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (tcbState obj) \<and> Structures_H.thread_state.Inactive \<noteq> tcbState obj \<and> Structures_H.thread_state.IdleThreadState \<noteq> tcbState obj) t 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_nonz_cap_to' t s
 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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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>); ko_wp_at' (case_option False (P \<circ> tcbState) \<circ> projectKO_opt) t (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> st_tcb_at' P t (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>)
 4. \<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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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); ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P (tcbState obj) \<and> Structures_H.thread_state.Inactive \<noteq> tcbState obj \<and> Structures_H.thread_state.IdleThreadState \<noteq> tcbState obj) t 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_nonz_cap_to' t s
 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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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>); ko_wp_at' (case_option False (P \<circ> tcbState) \<circ> projectKO_opt) t (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> st_tcb_at' P t (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>)
 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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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 (4 subgoals):
 1. \<And>s b obj. \<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; 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>); \<exists>obja. projectKO_opt obj = Some obja \<and> P (tcbState obja) \<and> Structures_H.thread_state.Inactive \<noteq> tcbState obja \<and> Structures_H.thread_state.IdleThreadState \<noteq> tcbState obja; ksPSpace s t = Some obj; is_aligned t (objBitsKO obj)\<rbrakk> \<Longrightarrow> live' obj
 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); 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> if_live_then_nonz_cap' s
 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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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>); ko_wp_at' (case_option False (P \<circ> tcbState) \<circ> projectKO_opt) t (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> st_tcb_at' P t (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>)
 4. \<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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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); 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> if_live_then_nonz_cap' s
 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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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>); ko_wp_at' (case_option False (P \<circ> tcbState) \<circ> projectKO_opt) t (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> st_tcb_at' P t (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>)
 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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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>); ko_wp_at' (case_option False (P \<circ> tcbState) \<circ> projectKO_opt) t (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> st_tcb_at' P t (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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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); st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t 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!