theory Orphanage

lemma sendIPC_valid_queues' [wp]:
  "\<lbrace> \<lambda>s. 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. valid_queues' s \<rbrace>" unfolding sendIPC_def apply (wpsimp wp: hoare_drop_imps) apply (wpsimp | wp (once) sts_st_tcb')+ apply (rule_tac Q="\<lambda>rv. valid_queues' and valid_objs' and ko_at' rv epptr
                          and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)" in hoare_post_imp) apply (clarsimp) apply (wp get_ep_sp' | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 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. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 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. valid_queues'\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>x21 x22 recvState. \<lbrace>?P'90 (Structures_H.endpoint.RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recvState () ()\<rbrace> setThreadState Structures_H.thread_state.Running x21 \<lbrace>\<lambda>rv s. st_tcb_at' runnable' x21 s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' runnable' x21 s\<rbrace>
 2. \<And>ep x1 x21 x22 x recvState xa. \<lbrakk>ep = Structures_H.endpoint.RecvEP x1; x1 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B38 ep x1 x21 x22 x recvState xa\<rbrace> doIPCTransfer thread (Just epptr) badge canGrant x21 \<lbrace>\<lambda>xb s. valid_queues' s \<and> ((\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> sch_act_simple s) \<and> sch_act_wf (ksSchedulerAction s) s) \<and> ?P'90 ep x1 x21 x22 x recvState xa xb s\<rbrace>
 3. \<And>ep x1 x21 x22 x recvState. \<lbrakk>ep = Structures_H.endpoint.RecvEP x1; x1 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B37 ep x1 x21 x22 x recvState\<rbrace> haskell_assert (isReceive recvState) [] \<lbrace>?B38 ep x1 x21 x22 x recvState\<rbrace>
 4. \<And>ep x1 x21 x22 x. \<lbrakk>ep = Structures_H.endpoint.RecvEP x1; x1 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B35 ep x1 x21 x22 x\<rbrace> getThreadState x21 \<lbrace>?B37 ep x1 x21 x22 x\<rbrace>
 5. \<And>ep x1 x21 x22. \<lbrakk>ep = Structures_H.endpoint.RecvEP x1; x1 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R29 ep x1 x21 x22\<rbrace> setEndpoint epptr $ case x22 of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.RecvEP x22 \<lbrace>?B35 ep x1 x21 x22\<rbrace>
 6. \<And>ep. ep = Structures_H.endpoint.IdleEP \<Longrightarrow> \<lbrace>?R15 ep\<rbrace> 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 () \<lbrace>\<lambda>rv. valid_queues'\<rbrace>
 7. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?R16 ep x3\<rbrace> if blocking then do setThreadState (Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply call) thread;
setEndpoint epptr $ Structures_H.endpoint.SendEP $ x3 @ [thread]
od else return () \<lbrace>\<lambda>rv. valid_queues'\<rbrace>
 8. \<lbrace>?Q1\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> (x = [] \<longrightarrow> valid_queues' s) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R29 ep x xa xb s)) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ?R15 ep s) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ?R16 ep x s)\<rbrace>
 9. \<And>s. valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> (x = [] \<longrightarrow> valid_queues' s) \<and> ((\<exists>xa xb. x = xa # xb) \<longrightarrow> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s)) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> valid_queues' s) \<and> ((\<exists>x. ep = Structures_H.endpoint.SendEP x) \<longrightarrow> valid_queues' s)\<rbrace>
 2. \<And>s. valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. (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> valid_queues' s) \<and> ((\<exists>xa xb. x = xa # xb) \<longrightarrow> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s)) \<and> (rv = Structures_H.endpoint.IdleEP \<longrightarrow> valid_queues' s) \<and> ((\<exists>x. rv = Structures_H.endpoint.SendEP x) \<longrightarrow> valid_queues' s)
 2. \<lbrace>?Q1\<rbrace> getEndpoint epptr \<lbrace>\<lambda>rv. valid_queues' and valid_objs' and ko_at' rv epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 3. \<And>s. valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> getEndpoint epptr \<lbrace>\<lambda>rv. valid_queues' and valid_objs' and ko_at' rv epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 2. \<And>s. valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> ?Q1 s proof (prove)
goal:
No subgoals!