theory Finalise_AI

lemma cancel_all_ipc_emptyable[wp]:
  "\<lbrace>invs and emptyable sl\<rbrace> cancel_all_ipc ptr \<lbrace>\<lambda>_. emptyable sl\<rbrace>" apply (simp add: cancel_all_ipc_def) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (case_tac ep, simp_all) apply (wp, simp) apply (wp cancel_all_emptyable_helper hoare_vcg_const_Ball_lift
        | simp add: get_ep_queue_def
        | clarsimp simp: invs_def valid_state_def valid_pspace_def
                         ep_queued_st_tcb_at)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and emptyable sl\<rbrace> cancel_all_ipc ptr \<lbrace>\<lambda>_. emptyable sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and emptyable sl\<rbrace> do ep <- get_endpoint ptr;
case ep of IdleEP \<Rightarrow> return () | _ \<Rightarrow> 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
od \<lbrace>\<lambda>_. emptyable sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ep. \<lbrace>ko_at (Endpoint ep) ptr and (invs and emptyable sl)\<rbrace> case ep of IdleEP \<Rightarrow> return () | _ \<Rightarrow> 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>_. emptyable sl\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>ko_at (Endpoint IdleEP) ptr and (invs and emptyable sl)\<rbrace> return () \<lbrace>\<lambda>_. emptyable sl\<rbrace>
 2. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>ko_at (Endpoint (SendEP x2)) ptr and (invs and emptyable sl)\<rbrace> do queue <- get_ep_queue (SendEP x2);
y <- set_endpoint ptr IdleEP;
y <- mapM_x (\<lambda>t. do y <- 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>_. emptyable sl\<rbrace>
 3. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ptr and (invs and emptyable sl)\<rbrace> do queue <- get_ep_queue (RecvEP x3);
y <- set_endpoint ptr IdleEP;
y <- mapM_x (\<lambda>t. do y <- 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>_. emptyable sl\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>ko_at (Endpoint (SendEP x2)) ptr and (invs and emptyable sl)\<rbrace> do queue <- get_ep_queue (SendEP x2);
y <- set_endpoint ptr IdleEP;
y <- mapM_x (\<lambda>t. do y <- 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>_. emptyable sl\<rbrace>
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ptr and (invs and emptyable sl)\<rbrace> do queue <- get_ep_queue (RecvEP x3);
y <- set_endpoint ptr IdleEP;
y <- mapM_x (\<lambda>t. do y <- 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>_. emptyable sl\<rbrace> proof (prove)
goal:
No subgoals!