theory Orphanage

lemma cancelAllIPC_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<rbrace>
    cancelAllIPC epptr
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding cancelAllIPC_def apply (wp sts_valid_objs' set_ep_valid_objs' sts_st_tcb'
            hoare_vcg_const_Ball_lift tcbSchedEnqueue_almost_no_orphans
             | wpc
             | rule mapM_x_match,
               rename_tac list,
               rule_tac V="\<lambda>_. valid_queues' and valid_objs'"
                    and I="no_orphans and (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s)"
                     in mapM_x_inv_wp2
             | clarsimp simp: valid_tcb_state'_def)+ apply (rule_tac Q="\<lambda>rv. no_orphans and valid_objs' and valid_queues' and ko_at' rv epptr"
                 in hoare_post_imp) apply (fastforce simp: valid_obj'_def valid_ep'_def obj_at'_def projectKOs) apply (wp get_ep_sp' | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> cancelAllIPC epptr \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> do ep <- getEndpoint epptr;
case ep of Structures_H.endpoint.IdleEP \<Rightarrow> return () | _ \<Rightarrow> do setEndpoint epptr Structures_H.endpoint.IdleEP;
forM_x (epQueue ep) (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> no_orphans s \<and> (\<forall>x\<in>set x. tcb_at' x s) \<and> valid_queues' s \<and> valid_objs' s \<and> valid_ep' Structures_H.endpoint.IdleEP s) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> no_orphans s) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> no_orphans s \<and> (\<forall>x\<in>set x. tcb_at' x s) \<and> valid_queues' s \<and> valid_objs' s \<and> valid_ep' Structures_H.endpoint.IdleEP s)\<rbrace>
 2. \<And>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. (no_orphans and valid_objs' and valid_queues' and ko_at' rv epptr) s \<Longrightarrow> (\<forall>x. rv = Structures_H.endpoint.RecvEP x \<longrightarrow> no_orphans s \<and> (\<forall>x\<in>set x. tcb_at' x s) \<and> valid_queues' s \<and> valid_objs' s \<and> valid_ep' Structures_H.endpoint.IdleEP s) \<and> (rv = Structures_H.endpoint.IdleEP \<longrightarrow> no_orphans s) \<and> (\<forall>x. rv = Structures_H.endpoint.SendEP x \<longrightarrow> no_orphans s \<and> (\<forall>x\<in>set x. tcb_at' x s) \<and> valid_queues' s \<and> valid_objs' s \<and> valid_ep' Structures_H.endpoint.IdleEP s)
 2. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>rv. no_orphans and valid_objs' and valid_queues' and ko_at' rv epptr\<rbrace>
 3. \<And>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>rv. no_orphans and valid_objs' and valid_queues' and ko_at' rv epptr\<rbrace>
 2. \<And>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!