theory Ipc_R

lemma cancelAllIPC_not_rct[wp]:
  "\<lbrace>\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<rbrace>
   cancelAllIPC epptr
   \<lbrace>\<lambda>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<rbrace>" apply (simp add: cancelAllIPC_def) apply (wp | wpc)+ apply (rule hoare_post_imp [OF _ rescheduleRequired_notresume], simp) apply simp apply (rule mapM_x_wp_inv) apply (wp)+ apply (rule hoare_post_imp [OF _ rescheduleRequired_notresume], simp) apply simp apply (rule mapM_x_wp_inv) apply (wp)+ apply (wp hoare_vcg_all_lift hoare_drop_imp) apply (simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace> cancelAllIPC epptr \<lbrace>\<lambda>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<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>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<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>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<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>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<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>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<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. ksSchedulerAction s \<noteq> ResumeCurrentThread \<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. ksSchedulerAction s \<noteq> ResumeCurrentThread\<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>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<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>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<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. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>ep x1. ep = Structures_H.endpoint.RecvEP x1 \<Longrightarrow> \<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. ksSchedulerAction s \<noteq> ResumeCurrentThread\<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>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<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>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<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. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>ep x1 x. ep = Structures_H.endpoint.RecvEP x1 \<Longrightarrow> \<lbrace>\<lambda>a. ksSchedulerAction a \<noteq> ResumeCurrentThread\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart x;
tcbSchedEnqueue x
od \<lbrace>\<lambda>xa a. ksSchedulerAction a \<noteq> ResumeCurrentThread\<rbrace>
 2. \<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. ksSchedulerAction b \<noteq> ResumeCurrentThread\<rbrace>
 3. \<And>ep. ep = Structures_H.endpoint.IdleEP \<Longrightarrow> \<lbrace>?R14 ep\<rbrace> return () \<lbrace>\<lambda>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<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>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<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. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>ep x3 x xa. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?B44 ep x3 x xa\<rbrace> rescheduleRequired \<lbrace>\<lambda>_ s. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace>
 2. \<And>ep x3 x. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?B42 ep x3 x\<rbrace> forM_x (epQueue ep) (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) \<lbrace>?B44 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>?B42 ep x3\<rbrace>
 4. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ?R15 ep x s)\<rbrace>
 5. \<And>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>ep x3 x. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?B42 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. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace>
 2. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?R15 ep x3\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>?B42 ep x3\<rbrace>
 3. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ?R15 ep x s)\<rbrace>
 4. \<And>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?B42 (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. ksSchedulerAction s \<noteq> ResumeCurrentThread\<rbrace>
 2. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?R15 ep x3\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>?B42 ep x3\<rbrace>
 3. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ?R15 ep x s)\<rbrace>
 4. \<And>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>ep x3 x. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>\<lambda>a. ksSchedulerAction a \<noteq> ResumeCurrentThread\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart x;
tcbSchedEnqueue x
od \<lbrace>\<lambda>xa a. ksSchedulerAction a \<noteq> ResumeCurrentThread\<rbrace>
 2. \<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. ksSchedulerAction b \<noteq> ResumeCurrentThread\<rbrace>
 3. \<lbrace>?Q\<rbrace> getEndpoint epptr \<lbrace>\<lambda>ep s. (\<forall>x. ep = Structures_H.endpoint.RecvEP x \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ?R15 ep x s)\<rbrace>
 4. \<And>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<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> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (ep = Structures_H.endpoint.IdleEP \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> (\<forall>x. ep = Structures_H.endpoint.SendEP x \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread)\<rbrace>
 2. \<And>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ksSchedulerAction s \<noteq> ResumeCurrentThread \<Longrightarrow> (\<forall>x. ksSchedulerAction s \<noteq> ResumeCurrentThread) \<and> ksSchedulerAction s \<noteq> ResumeCurrentThread \<and> (\<forall>x. ksSchedulerAction s \<noteq> ResumeCurrentThread) proof (prove)
goal:
No subgoals!