theory Orphanage

lemma sendSignal_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>
   sendSignal ntfnptr badge
   \<lbrace> \<lambda>_ s. no_orphans s \<rbrace>" unfolding sendSignal_def apply (rule hoare_pre) apply (wp sts_st_tcb' gts_wp' getNotification_wp asUser_almost_no_orphans
                          cancelIPC_weak_sch_act_wf
          | wpc | clarsimp simp: sch_act_wf_weak)+ 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> sendSignal ntfnptr badge \<lbrace>\<lambda>_. 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 nTFN <- getNotification ntfnptr;
case (ntfnObj nTFN, ntfnBoundTCB nTFN) of (Structures_H.ntfn.IdleNtfn, None) \<Rightarrow> setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN | (Structures_H.ntfn.IdleNtfn, Some tcb) \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do cancelIPC tcb;
setThreadState Structures_H.thread_state.Running tcb;
asUser tcb $ setRegister Notification_H.badgeRegister badge;
possibleSwitchTo tcb
od else setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN
od | (Structures_H.ntfn.ActiveNtfn badge', x) \<Rightarrow> do newBadge <- return (badge || badge');
setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn newBadge) nTFN
od | (Structures_H.ntfn.WaitingNtfn [], x) \<Rightarrow> haskell_fail [] | (Structures_H.ntfn.WaitingNtfn (dest # queue), x) \<Rightarrow> do setNotification ntfnptr $ ntfnObj_update (\<lambda>_. case queue of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn queue) nTFN;
setThreadState Structures_H.thread_state.Running dest;
asUser dest $ setRegister Notification_H.badgeRegister badge;
possibleSwitchTo dest
od
od \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do nTFN <- getNotification ntfnptr;
case (ntfnObj nTFN, ntfnBoundTCB nTFN) of (Structures_H.ntfn.IdleNtfn, None) \<Rightarrow> setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN | (Structures_H.ntfn.IdleNtfn, Some tcb) \<Rightarrow> do state <- getThreadState tcb;
if receiveBlocked state then do cancelIPC tcb;
setThreadState Structures_H.thread_state.Running tcb;
asUser tcb $ setRegister Notification_H.badgeRegister badge;
possibleSwitchTo tcb
od else setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) nTFN
od | (Structures_H.ntfn.ActiveNtfn badge', x) \<Rightarrow> do newBadge <- return (badge || badge');
setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn newBadge) nTFN
od | (Structures_H.ntfn.WaitingNtfn [], x) \<Rightarrow> haskell_fail [] | (Structures_H.ntfn.WaitingNtfn (dest # queue), x) \<Rightarrow> do setNotification ntfnptr $ ntfnObj_update (\<lambda>_. case queue of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> Structures_H.ntfn.WaitingNtfn queue) nTFN;
setThreadState Structures_H.thread_state.Running dest;
asUser dest $ setRegister Notification_H.badgeRegister badge;
possibleSwitchTo dest
od
od \<lbrace>\<lambda>_. no_orphans\<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!