theory IpcCancel_AI

lemma cancel_all_ipc_unlive[wp]:
  "\<lbrace>\<top>\<rbrace> cancel_all_ipc ptr \<lbrace>\<lambda> rv. obj_at (Not \<circ> live) ptr\<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: set_simple_ko_def get_ep_queue_def) apply wp apply (clarsimp simp: live_def elim!: obj_at_weakenE) apply (wp cancel_all_unlive_helper set_object_at_obj3 | simp only: obj_at_exst_update)+ apply (clarsimp simp: live_def) apply (wp cancel_all_unlive_helper set_object_at_obj3 | simp only: obj_at_exst_update)+ apply (clarsimp simp: live_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> cancel_all_ipc ptr \<lbrace>\<lambda>rv. obj_at (Not \<circ> live) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<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>rv. obj_at (Not \<circ> live) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ep. \<lbrace>ko_at (Endpoint ep) ptr and (\<lambda>_. True)\<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>rv. obj_at (Not \<circ> live) ptr\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>ko_at (Endpoint IdleEP) ptr\<rbrace> return () \<lbrace>\<lambda>rv. obj_at (Not \<circ> live) ptr\<rbrace>
 2. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>ko_at (Endpoint (SendEP x2)) ptr\<rbrace> do y <- do obj <- get_object ptr;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. Endpoint y = obj);
set_object ptr (Endpoint IdleEP)
od;
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>rv. obj_at (Not \<circ> live) ptr\<rbrace>
 3. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ptr\<rbrace> do y <- do obj <- get_object ptr;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. Endpoint y = obj);
set_object ptr (Endpoint IdleEP)
od;
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>rv. obj_at (Not \<circ> live) ptr\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. ko_at (Endpoint IdleEP) ptr s \<Longrightarrow> obj_at (Not \<circ> live) ptr s
 2. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>ko_at (Endpoint (SendEP x2)) ptr\<rbrace> do y <- do obj <- get_object ptr;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. Endpoint y = obj);
set_object ptr (Endpoint IdleEP)
od;
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>rv. obj_at (Not \<circ> live) ptr\<rbrace>
 3. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ptr\<rbrace> do y <- do obj <- get_object ptr;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. Endpoint y = obj);
set_object ptr (Endpoint IdleEP)
od;
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>rv. obj_at (Not \<circ> live) ptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>ko_at (Endpoint (SendEP x2)) ptr\<rbrace> do y <- do obj <- get_object ptr;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. Endpoint y = obj);
set_object ptr (Endpoint IdleEP)
od;
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>rv. obj_at (Not \<circ> live) ptr\<rbrace>
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ptr\<rbrace> do y <- do obj <- get_object ptr;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. Endpoint y = obj);
set_object ptr (Endpoint IdleEP)
od;
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>rv. obj_at (Not \<circ> live) ptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ep x2 s. \<lbrakk>ep = SendEP x2; ko_at (Endpoint (SendEP x2)) ptr s\<rbrakk> \<Longrightarrow> K (\<not> live (Endpoint IdleEP) \<and> (\<forall>tcb. Endpoint IdleEP \<noteq> TCB tcb)) s
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ptr\<rbrace> do y <- do obj <- get_object ptr;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. Endpoint y = obj);
set_object ptr (Endpoint IdleEP)
od;
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>rv. obj_at (Not \<circ> live) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ptr\<rbrace> do y <- do obj <- get_object ptr;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. Endpoint y = obj);
set_object ptr (Endpoint IdleEP)
od;
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>rv. obj_at (Not \<circ> live) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ep x3 s. \<lbrakk>ep = RecvEP x3; ko_at (Endpoint (RecvEP x3)) ptr s\<rbrakk> \<Longrightarrow> K (\<not> live (Endpoint IdleEP) \<and> (\<forall>tcb. Endpoint IdleEP \<noteq> TCB tcb)) s proof (prove)
goal:
No subgoals!