theory Orphanage

lemma cancelBadgedSends_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> valid_queues' s \<rbrace>
   cancelBadgedSends epptr badge
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding cancelBadgedSends_def apply (rule hoare_pre) apply (wp hoare_drop_imps | wpc | clarsimp)+ apply (wp filterM_preserved tcbSchedEnqueue_almost_no_orphans gts_wp'
                sts_st_tcb' hoare_drop_imps | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s\<rbrace> cancelBadgedSends epptr badge \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s\<rbrace> do ep <- getEndpoint epptr;
case ep of Structures_H.endpoint.SendEP queue \<Rightarrow> do setEndpoint epptr Structures_H.endpoint.IdleEP;
queue' <- swp filterM queue (\<lambda>t. do st <- getThreadState t;
if blockingIPCBadge st = badge then do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t;
return False
od else return True
od);
ep' <- case queue' of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ Structures_H.endpoint.SendEP queue';
setEndpoint epptr ep';
rescheduleRequired
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do ep <- getEndpoint epptr;
case ep of Structures_H.endpoint.SendEP queue \<Rightarrow> do setEndpoint epptr Structures_H.endpoint.IdleEP;
queue' <- swp filterM queue (\<lambda>t. do st <- getThreadState t;
if blockingIPCBadge st = badge then do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t;
return False
od else return True
od);
ep' <- case queue' of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ Structures_H.endpoint.SendEP queue';
setEndpoint epptr ep';
rescheduleRequired
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>s. no_orphans s \<and> valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>x3. \<lbrace>?P59 (Structures_H.endpoint.SendEP x3) x3 ()\<rbrace> filterM (\<lambda>t. do st <- getThreadState t;
if blockingIPCBadge st = badge then do y <- setThreadState Structures_H.thread_state.Restart t;
y <- tcbSchedEnqueue t;
return False
od else return True
od) x3 \<lbrace>\<lambda>rv s. no_orphans s \<and> valid_queues' s\<rbrace>
 2. \<And>ep x3 x. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?P'59 ep x3 x\<rbrace> swp filterM x3 (\<lambda>t. do st <- getThreadState t;
if blockingIPCBadge st = badge then do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t;
return False
od else return True
od) \<lbrace>\<lambda>rv s. \<forall>x xa. rv = x # xa \<longrightarrow> no_orphans s \<and> valid_queues' s\<rbrace>
 3. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?R19 ep x3\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>x s. ?P59 ep x3 x s \<and> ?P'59 ep x3 x s\<rbrace>
 4. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> no_orphans s) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> no_orphans s) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ?R19 ep x s)\<rbrace>
 5. \<And>s. no_orphans s \<and> valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!