theory Orphanage

lemma deleteObjects_no_orphans [wp]:
  "\<lbrace> (\<lambda>s. no_orphans s \<and> pspace_distinct' s) and K (is_aligned ptr bits) \<rbrace>
   deleteObjects ptr bits
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" apply (rule hoare_gen_asm) apply (unfold deleteObjects_def2 doMachineOp_def split_def) apply (wp hoare_drop_imps | clarsimp)+ apply (clarsimp simp: no_orphans_def all_active_tcb_ptrs_def
                        all_queued_tcb_ptrs_def is_active_tcb_ptr_def
                        ksMachineState_ksPSpace_upd_comm) apply (drule_tac x=tcb_ptr in spec) apply (clarsimp simp: pred_tcb_at'_def obj_at_delete'[simplified field_simps]
                  cong: if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. no_orphans s \<and> pspace_distinct' s) and K (is_aligned ptr bits)\<rbrace> deleteObjects ptr bits \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned ptr bits \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> pspace_distinct' s\<rbrace> deleteObjects ptr bits \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned ptr bits \<Longrightarrow> \<lbrace>\<lambda>s. no_orphans s \<and> pspace_distinct' s\<rbrace> do stateAssert (deletionIsSafe ptr bits) [];
do ms <- gets ksMachineState;
p <- select_f (freeMemory ptr bits ms);
modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od;
stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. x \<in> {ptr..ptr + 2 ^ bits - 1})) [];
modify (\<lambda>s. s\<lparr>ksPSpace := \<lambda>x. if x \<in> {ptr..ptr + 2 ^ bits - 1} then None else ksPSpace s x, gsUserPages := \<lambda>x. if x \<in> {ptr..ptr + 2 ^ bits - 1} then None else gsUserPages s x, gsCNodes := \<lambda>x. if x \<in> {ptr..ptr + 2 ^ bits - 1} then None else gsCNodes s x\<rparr>);
stateAssert ksASIDMapSafe []
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>is_aligned ptr bits; no_orphans s; pspace_distinct' s; deletionIsSafe ptr bits s; ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s))\<rbrakk> \<Longrightarrow> no_orphans (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>) proof (prove)
goal (1 subgoal):
 1. \<And>s b tcb_ptr. \<lbrakk>is_aligned ptr bits; \<forall>tcb_ptr. st_tcb_at' is_active_thread_state tcb_ptr s \<longrightarrow> tcb_ptr = ksCurThread s \<or> (\<exists>a b. tcb_ptr \<in> set (ksReadyQueues s (a, b))) \<or> ksSchedulerAction s = SwitchToThread tcb_ptr; pspace_distinct' s; deletionIsSafe ptr bits s; ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); st_tcb_at' is_active_thread_state tcb_ptr (s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x\<rparr>); tcb_ptr \<noteq> ksCurThread s; sch_act_not tcb_ptr s\<rbrakk> \<Longrightarrow> \<exists>a b. tcb_ptr \<in> set (ksReadyQueues s (a, b)) proof (prove)
goal (1 subgoal):
 1. \<And>s b tcb_ptr. \<lbrakk>is_aligned ptr bits; pspace_distinct' s; deletionIsSafe ptr bits s; ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); st_tcb_at' is_active_thread_state tcb_ptr (s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x\<rparr>); tcb_ptr \<noteq> ksCurThread s; sch_act_not tcb_ptr s; st_tcb_at' is_active_thread_state tcb_ptr s \<longrightarrow> tcb_ptr = ksCurThread s \<or> (\<exists>a b. tcb_ptr \<in> set (ksReadyQueues s (a, b))) \<or> ksSchedulerAction s = SwitchToThread tcb_ptr\<rbrakk> \<Longrightarrow> \<exists>a b. tcb_ptr \<in> set (ksReadyQueues s (a, b)) proof (prove)
goal:
No subgoals!