theory IpcCancel_AI

lemma cancel_all_ipc_valid_objs:
  "\<lbrace>valid_objs and (\<lambda>s. sym_refs (state_refs_of s))\<rbrace>
   cancel_all_ipc ptr \<lbrace>\<lambda>_. valid_objs\<rbrace>" apply (simp add: cancel_all_ipc_def) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (case_tac ep, simp_all add: get_ep_queue_def) apply (wp, simp) apply (wp cancel_all_helper hoare_vcg_const_Ball_lift
        | clarsimp simp: ep_queued_st_tcb_at obj_at_def valid_ep_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and (\<lambda>s. sym_refs (state_refs_of s))\<rbrace> cancel_all_ipc ptr \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and (\<lambda>s. sym_refs (state_refs_of s))\<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>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ep. \<lbrace>ko_at (Endpoint ep) ptr and (valid_objs and (\<lambda>s. sym_refs (state_refs_of s)))\<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>_. valid_objs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>ko_at (Endpoint IdleEP) ptr and (valid_objs and (\<lambda>s. sym_refs (state_refs_of s)))\<rbrace> return () \<lbrace>\<lambda>_. valid_objs\<rbrace>
 2. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>ko_at (Endpoint (SendEP x2)) ptr and (valid_objs and (\<lambda>s. sym_refs (state_refs_of s)))\<rbrace> do 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) x2;
do_extended_op reschedule_required
od \<lbrace>\<lambda>_. valid_objs\<rbrace>
 3. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ptr and (valid_objs and (\<lambda>s. sym_refs (state_refs_of s)))\<rbrace> do 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) x3;
do_extended_op reschedule_required
od \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>ko_at (Endpoint (SendEP x2)) ptr and (valid_objs and (\<lambda>s. sym_refs (state_refs_of s)))\<rbrace> do 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) x2;
do_extended_op reschedule_required
od \<lbrace>\<lambda>_. valid_objs\<rbrace>
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ptr and (valid_objs and (\<lambda>s. sym_refs (state_refs_of s)))\<rbrace> do 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) x3;
do_extended_op reschedule_required
od \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal:
No subgoals!