theory Syscall_AC

lemma cancel_all_ipc_ct_active[wp]:
  "cancel_all_ipc ptr \<lbrace>ct_active\<rbrace>" apply (wp mapM_x_wp set_simple_ko_ct_active | wps | simp add: cancel_all_ipc_def | wpc)+ apply force apply (wp mapM_x_wp set_simple_ko_ct_active)+ apply force apply (wp set_simple_ko_ct_active hoare_drop_imps hoare_vcg_conj_lift hoare_vcg_all_lift)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_active\<rbrace> cancel_all_ipc ptr \<lbrace>\<lambda>_. ct_active\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ep x2 queue. ep = SendEP x2 \<Longrightarrow> set queue \<subseteq> ?S29 (SendEP x2) x2 queue ()
 2. \<And>ep x2 queue. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B22 ep x2 queue\<rbrace> set_endpoint ptr IdleEP \<lbrace>\<lambda>x. ct_active\<rbrace>
 3. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R14 ep x2\<rbrace> get_ep_queue ep \<lbrace>?B22 ep x2\<rbrace>
 4. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R15 ep x3\<rbrace> do queue <- get_ep_queue ep;
set_endpoint ptr IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od \<lbrace>\<lambda>_. ct_active\<rbrace>
 5. \<lbrace>?Q\<rbrace> get_endpoint ptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> ct_active s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R14 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R15 ep x s)\<rbrace>
 6. \<And>s. ct_active s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>ep x2 queue. ep = SendEP x2 \<Longrightarrow> \<lbrace>?B22 ep x2 queue\<rbrace> set_endpoint ptr IdleEP \<lbrace>\<lambda>x. ct_active\<rbrace>
 2. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?R14 ep x2\<rbrace> get_ep_queue ep \<lbrace>?B22 ep x2\<rbrace>
 3. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R15 ep x3\<rbrace> do queue <- get_ep_queue ep;
set_endpoint ptr IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od \<lbrace>\<lambda>_. ct_active\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_endpoint ptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> ct_active s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R14 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R15 ep x s)\<rbrace>
 5. \<And>s. ct_active s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>ep x3 queue x. ep = RecvEP x3 \<Longrightarrow> set queue \<subseteq> ?S54 ep x3 queue x
 2. \<And>ep x3 queue. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?B47 ep x3 queue\<rbrace> set_endpoint ptr IdleEP \<lbrace>\<lambda>x. ct_active\<rbrace>
 3. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R15 ep x3\<rbrace> get_ep_queue ep \<lbrace>?B47 ep x3\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_endpoint ptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> ct_active s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ct_active s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R15 ep x s)\<rbrace>
 5. \<And>s. ct_active s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>ep x3 queue. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?B47 ep x3 queue\<rbrace> set_endpoint ptr IdleEP \<lbrace>\<lambda>x. ct_active\<rbrace>
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>?R15 ep x3\<rbrace> get_ep_queue ep \<lbrace>?B47 ep x3\<rbrace>
 3. \<lbrace>?Q\<rbrace> get_endpoint ptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> ct_active s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ct_active s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R15 ep x s)\<rbrace>
 4. \<And>s. ct_active s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ct_active s \<Longrightarrow> ct_active s \<and> (\<forall>x. ct_active s) \<and> (\<forall>x. ct_active s) proof (prove)
goal:
No subgoals!