theory Finalise_R

lemma cancelAllIPC_ct_not_ksQ:
  "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane
          and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace>
   cancelAllIPC epptr
   \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>"
  (is "\<lbrace>?PRE\<rbrace> _ \<lbrace>\<lambda>_. ?POST\<rbrace>") apply (simp add: cancelAllIPC_def) apply (wp, wpc, wp) apply (wps rescheduleRequired_ct') apply (wp rescheduleRequired_ksQ') apply clarsimp apply (wp cancelAll_ct_not_ksQ_helper mapM_x_wp_inv) apply (wp hoare_lift_Pf2 [OF setEndpoint_ksQ setEndpoint_ct'])+ apply (wps rescheduleRequired_ct') apply (wp rescheduleRequired_ksQ') apply clarsimp apply (wp cancelAll_ct_not_ksQ_helper mapM_x_wp_inv) apply (wp hoare_lift_Pf2 [OF setEndpoint_ksQ setEndpoint_ct'])+ prefer 2 apply assumption apply (rule_tac Q="\<lambda>ep. ?PRE and ko_at' ep epptr" in hoare_post_imp) apply (clarsimp) apply (rule conjI) apply ((clarsimp simp: invs'_def valid_state'_def
                           sch_act_sane_def
            | drule(1) ct_not_in_epQueue)+)[2] apply (wp get_ep_sp') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> cancelAllIPC epptr \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<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 s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>ep x1 x xa. ep = Structures_H.endpoint.RecvEP x1 \<Longrightarrow> \<lbrace>?B21 ep x1 x xa\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<And>ep x1 x. ep = Structures_H.endpoint.RecvEP x1 \<Longrightarrow> \<lbrace>?B19 ep x1 x\<rbrace> forM_x (epQueue ep) (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) \<lbrace>?B21 ep x1 x\<rbrace>
 3. \<And>ep x1. ep = Structures_H.endpoint.RecvEP x1 \<Longrightarrow> \<lbrace>?R13 ep x1\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>?B19 ep x1\<rbrace>
 4. \<And>ep. ep = Structures_H.endpoint.IdleEP \<Longrightarrow> \<lbrace>?R14 ep\<rbrace> return () \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 5. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?R15 ep x3\<rbrace> 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 \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 6. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> ?R13 ep x s) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ?R14 ep s) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ?R15 ep x s)\<rbrace>
 7. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>ep x1 x xa prev_s. ep = Structures_H.endpoint.RecvEP x1 \<Longrightarrow> \<lbrace>?P24 ep x1 x xa prev_s\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv s'. ksCurThread prev_s \<notin> set (ksReadyQueues s' p)\<rbrace>
 2. \<And>ep x1 x. ep = Structures_H.endpoint.RecvEP x1 \<Longrightarrow> \<lbrace>?B19 ep x1 x\<rbrace> forM_x (epQueue ep) (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) \<lbrace>\<lambda>xa s. ?P24 ep x1 x xa s s\<rbrace>
 3. \<And>ep x1. ep = Structures_H.endpoint.RecvEP x1 \<Longrightarrow> \<lbrace>?R13 ep x1\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>?B19 ep x1\<rbrace>
 4. \<And>ep. ep = Structures_H.endpoint.IdleEP \<Longrightarrow> \<lbrace>?R14 ep\<rbrace> return () \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 5. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?R15 ep x3\<rbrace> 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 \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 6. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> ?R13 ep x s) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ?R14 ep s) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ?R15 ep x s)\<rbrace>
 7. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>ep x1 x. ep = Structures_H.endpoint.RecvEP x1 \<Longrightarrow> \<lbrace>?B19 ep x1 x\<rbrace> forM_x (epQueue ep) (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) \<lbrace>\<lambda>xa s. ksCurThread s \<notin> set (ksReadyQueues s p) \<and> sch_act_not (ksCurThread s) s\<rbrace>
 2. \<And>ep x1. ep = Structures_H.endpoint.RecvEP x1 \<Longrightarrow> \<lbrace>?R13 ep x1\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>?B19 ep x1\<rbrace>
 3. \<And>ep. ep = Structures_H.endpoint.IdleEP \<Longrightarrow> \<lbrace>?R14 ep\<rbrace> return () \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 4. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?R15 ep x3\<rbrace> 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 \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 5. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> ?R13 ep x s) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ?R14 ep s) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ?R15 ep x s)\<rbrace>
 6. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>x1. \<lbrace>?B19 (Structures_H.endpoint.RecvEP x1) x1 ()\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x1 \<lbrace>\<lambda>xa s. ksCurThread s \<notin> set (ksReadyQueues s p) \<and> sch_act_not (ksCurThread s) s\<rbrace>
 2. \<And>ep x1. ep = Structures_H.endpoint.RecvEP x1 \<Longrightarrow> \<lbrace>?R13 ep x1\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>?B19 ep x1\<rbrace>
 3. \<And>ep. ep = Structures_H.endpoint.IdleEP \<Longrightarrow> \<lbrace>?R14 ep\<rbrace> return () \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 4. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?R15 ep x3\<rbrace> 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 \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 5. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> ?R13 ep x s) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ?R14 ep s) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ?R15 ep x s)\<rbrace>
 6. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>ep x1. ep = Structures_H.endpoint.RecvEP x1 \<Longrightarrow> \<lbrace>?R13 ep x1\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>a b. ((\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and (\<lambda>s. ksCurThread s \<notin> set x1)) b \<and> sch_act_not (ksCurThread b) b\<rbrace>
 2. \<And>ep. ep = Structures_H.endpoint.IdleEP \<Longrightarrow> \<lbrace>?R14 ep\<rbrace> return () \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 3. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?R15 ep x3\<rbrace> 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 \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 4. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> ?R13 ep x s) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ?R14 ep s) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ?R15 ep x s)\<rbrace>
 5. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>ep x3 x xa. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?B84 ep x3 x xa\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<And>ep x3 x. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?B82 ep x3 x\<rbrace> forM_x (epQueue ep) (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) \<lbrace>?B84 ep x3 x\<rbrace>
 3. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?R15 ep x3\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>?B82 ep x3\<rbrace>
 4. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ?R15 ep x s)\<rbrace>
 5. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>ep x3 x xa prev_s. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?P87 ep x3 x xa prev_s\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv s'. ksCurThread prev_s \<notin> set (ksReadyQueues s' p)\<rbrace>
 2. \<And>ep x3 x. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?B82 ep x3 x\<rbrace> forM_x (epQueue ep) (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) \<lbrace>\<lambda>xa s. ?P87 ep x3 x xa s s\<rbrace>
 3. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?R15 ep x3\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>?B82 ep x3\<rbrace>
 4. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ?R15 ep x s)\<rbrace>
 5. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>ep x3 x. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?B82 ep x3 x\<rbrace> forM_x (epQueue ep) (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) \<lbrace>\<lambda>xa s. ksCurThread s \<notin> set (ksReadyQueues s p) \<and> sch_act_not (ksCurThread s) s\<rbrace>
 2. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?R15 ep x3\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>?B82 ep x3\<rbrace>
 3. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ?R15 ep x s)\<rbrace>
 4. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>x3. \<lbrace>?B82 (Structures_H.endpoint.SendEP x3) x3 ()\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) x3 \<lbrace>\<lambda>xa s. ksCurThread s \<notin> set (ksReadyQueues s p) \<and> sch_act_not (ksCurThread s) s\<rbrace>
 2. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?R15 ep x3\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>?B82 ep x3\<rbrace>
 3. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ?R15 ep x s)\<rbrace>
 4. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?R15 ep x3\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>a b. ((\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and (\<lambda>s. ksCurThread s \<notin> set x3)) b \<and> sch_act_not (ksCurThread b) b\<rbrace>
 2. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ?R15 ep x s)\<rbrace>
 3. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s)\<rbrace>
 2. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s
 2. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and ko_at' rv epptr) s \<Longrightarrow> (\<forall>x. rv = Structures_H.endpoint.RecvEP x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s) \<and> (rv = Structures_H.endpoint.IdleEP \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> (\<forall>x. rv = Structures_H.endpoint.SendEP x \<longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) \<and> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s)
 2. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep. invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and ko_at' ep epptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>invs' s; ct_in_state' simple' s; sch_act_sane s; ksCurThread s \<notin> set (ksReadyQueues s p); ko_at' rv epptr s\<rbrakk> \<Longrightarrow> (\<forall>x. rv = Structures_H.endpoint.RecvEP x \<longrightarrow> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s) \<and> (\<forall>x. rv = Structures_H.endpoint.SendEP x \<longrightarrow> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s)
 2. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep. invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and ko_at' ep epptr\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>invs' s; ct_in_state' simple' s; sch_act_sane s; ksCurThread s \<notin> set (ksReadyQueues s p); ko_at' rv epptr s\<rbrakk> \<Longrightarrow> \<forall>x. rv = Structures_H.endpoint.RecvEP x \<longrightarrow> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s
 2. \<And>rv s. \<lbrakk>invs' s; ct_in_state' simple' s; sch_act_sane s; ksCurThread s \<notin> set (ksReadyQueues s p); ko_at' rv epptr s\<rbrakk> \<Longrightarrow> \<forall>x. rv = Structures_H.endpoint.SendEP x \<longrightarrow> ksCurThread s \<notin> set x \<and> sch_act_not (ksCurThread s) s
 3. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep. invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and ko_at' ep epptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep. invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and ko_at' ep epptr\<rbrace> proof (prove)
goal:
No subgoals!