theory Orphanage

lemma sendIPC_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<rbrace>
   sendIPC blocking call badge canGrant canGrantReply thread epptr
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding sendIPC_def apply (wp hoare_drop_imps setThreadState_not_active_no_orphans sts_st_tcb'
            possibleSwitchTo_almost_no_orphans'
         | wpc
         | clarsimp simp: is_active_thread_state_def isRestart_def isRunning_def)+ apply (rule_tac Q="\<lambda>rv. no_orphans and valid_queues' and valid_objs' and ko_at' rv epptr
                          and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)" in hoare_post_imp) apply (fastforce simp: valid_objs'_def 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 \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace> sendIPC blocking call badge canGrant canGrantReply thread 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 \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace> do ep <- getEndpoint epptr;
case ep of Structures_H.endpoint.RecvEP [] \<Rightarrow> haskell_fail [] | Structures_H.endpoint.RecvEP (dest # queue) \<Rightarrow> do setEndpoint epptr $ case queue of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.RecvEP queue;
recvState <- getThreadState dest;
haskell_assert (isReceive recvState) [];
doIPCTransfer thread (Just epptr) badge canGrant dest;
setThreadState Structures_H.thread_state.Running dest;
possibleSwitchTo dest;
case (call, canGrant \<or> canGrantReply) of (True, True) \<Rightarrow> setupCallerCap thread dest (blockingIPCCanGrant recvState) | (True, False) \<Rightarrow> setThreadState Structures_H.thread_state.Inactive thread | (False, xa) \<Rightarrow> return ()
od | Structures_H.endpoint.IdleEP \<Rightarrow> if blocking then do setThreadState (Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply call) thread;
setEndpoint epptr $ Structures_H.endpoint.SendEP [thread]
od else return () | Structures_H.endpoint.SendEP queue \<Rightarrow> if blocking then do setThreadState (Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply call) thread;
setEndpoint epptr $ Structures_H.endpoint.SendEP $ queue @ [thread]
od else return ()
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> (x = [] \<longrightarrow> no_orphans s) \<and> ((\<exists>xa xb. x = xa # xb) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> no_orphans s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> no_orphans s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s)) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> (blocking \<longrightarrow> no_orphans s \<and> valid_queues' s) \<and> (\<not> blocking \<longrightarrow> no_orphans s)) \<and> ((\<exists>x. ep = Structures_H.endpoint.SendEP x) \<longrightarrow> (blocking \<longrightarrow> no_orphans s \<and> valid_queues' s) \<and> (\<not> blocking \<longrightarrow> no_orphans s))\<rbrace>
 2. \<And>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. (no_orphans and valid_queues' and valid_objs' and ko_at' rv epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> (\<forall>x. rv = Structures_H.endpoint.RecvEP x \<longrightarrow> (x = [] \<longrightarrow> no_orphans s) \<and> ((\<exists>xa xb. x = xa # xb) \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> no_orphans s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> no_orphans s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s)) \<and> (rv = Structures_H.endpoint.IdleEP \<longrightarrow> (blocking \<longrightarrow> no_orphans s \<and> valid_queues' s) \<and> (\<not> blocking \<longrightarrow> no_orphans s)) \<and> ((\<exists>x. rv = Structures_H.endpoint.SendEP x) \<longrightarrow> (blocking \<longrightarrow> no_orphans s \<and> valid_queues' s) \<and> (\<not> blocking \<longrightarrow> no_orphans s))
 2. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>rv. no_orphans and valid_queues' and valid_objs' and ko_at' rv epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 3. \<And>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>rv. no_orphans and valid_queues' and valid_objs' and ko_at' rv epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 2. \<And>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!