theory Ipc_IF

lemma blocked_cancel_ipc_nosts_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "reads_respects aag l
     (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = (BlockedOnReceive x pl)) t
                      and bound_tcb_at ((=) (Some ntfnptr)) t
                      and (\<lambda>s. is_subject aag (cur_thread s))
                      and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag
                           \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag
                           \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag))
     (blocked_cancel_ipc_nosts t)" unfolding blocked_cancel_ipc_nosts_def apply (simp only:bind_assoc[symmetric]) apply (rule bind_ev[where P''=\<top>,simplified]) apply (wp set_thread_state_runnable_reads_respects,simp) subgoal proof (cases "aag_can_read_label aag (pasObjectAbs aag x) \<or> aag_can_affect aag l x") case True thus ?thesis \<comment> \<open>boring case, can read or affect ep\<close> unfolding blocked_cancel_ipc_nosts_def get_blocking_object_def apply clarsimp apply (rule pre_ev) apply (wpsimp wp: set_thread_state_reads_respects get_ep_queue_reads_respects
                         get_simple_ko_reads_respects get_blocking_object_reads_respects
                         gts_reads_respects set_simple_ko_reads_respects gts_wp
                   simp: get_blocking_object_def get_thread_state_rev)+ apply (clarsimp simp: pred_tcb_at_def obj_at_def) by (fastforce dest:read_sync_ep_read_receivers ) next case False thus ?thesis apply -  \<comment> \<open>can't read or affect ep\<close> apply (rule gen_asm_ev) apply (drule label_is_invisible[THEN iffD2]) apply clarsimp apply (rule ev2_invisible_simple[OF domains_distinct],assumption) apply (simp add: get_blocking_object_def) apply (rule modifies_at_mostI) apply (rule hoare_pre) apply (wpsimp wp: set_thread_state_runnable_equiv_but_for_labels
                         set_endpoint_equiv_but_for_labels get_object_wp gts_wp
                         set_thread_state_runnable_equiv_but_for_labels)+ by (fastforce simp: pred_tcb_at_def obj_at_def) qed by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (blocked_cancel_ipc_nosts t) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (do state <- get_thread_state t;
epptr <- get_blocking_object state;
ep <- get_endpoint epptr;
queue <- get_ep_queue ep;
queue' <- return $ remove1 t queue;
ep' <- return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue');
set_endpoint epptr ep';
set_thread_state t Running
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (do do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od;
set_thread_state t Running
od) proof (prove)
goal (3 subgoals):
 1. \<And>rv. reads_respects aag l (?Q rv) (K_bind (set_thread_state t Running) rv)
 2. reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od)
 3. \<lbrace>\<lambda>_. True\<rbrace> do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od)
 2. \<lbrace>\<lambda>_. True\<rbrace> do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od \<lbrace>\<lambda>rv _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od) proof (state)
goal (2 subgoals):
 1. aag_can_read_or_affect aag l x \<Longrightarrow> reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od)
 2. \<not> aag_can_read_or_affect aag l x \<Longrightarrow> reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od) proof (state)
this:
aag_can_read_or_affect aag l x

goal (2 subgoals):
 1. aag_can_read_or_affect aag l x \<Longrightarrow> reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od)
 2. \<not> aag_can_read_or_affect aag l x \<Longrightarrow> reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od) proof (prove)
using this:
aag_can_read_or_affect aag l x

goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od) proof (prove)
using this:
aag_can_read_or_affect aag l x

goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (do epptr <- do state <- get_thread_state t;
case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail
od;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od) proof (prove)
goal (1 subgoal):
 1. aag_can_read_or_affect aag l x \<Longrightarrow> reads_respects aag l (\<lambda>s. pas_refined aag s \<and> st_tcb_at (\<lambda>st. st = BlockedOnReceive x pl) t s \<and> bound_tcb_at ((=) (Some ntfnptr)) t s \<and> is_subject aag (cur_thread s) \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag) (do epptr <- do state <- get_thread_state t;
case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail
od;
do ep <- get_endpoint epptr;
queue <- get_ep_queue ep;
return (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))
od >>= set_endpoint epptr
od) proof (prove)
goal (2 subgoals):
 1. aag_can_read_or_affect aag l x \<Longrightarrow> reads_respects aag l ?Q2 (do epptr <- do state <- get_thread_state t;
case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail
od;
do ep <- get_endpoint epptr;
queue <- get_ep_queue ep;
return (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))
od >>= set_endpoint epptr
od)
 2. \<And>s. \<lbrakk>aag_can_read_or_affect aag l x; pas_refined aag s \<and> st_tcb_at (\<lambda>st. st = BlockedOnReceive x pl) t s \<and> bound_tcb_at ((=) (Some ntfnptr)) t s \<and> is_subject aag (cur_thread s) \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>aag_can_read_or_affect aag l x; pas_refined aag s; st_tcb_at (\<lambda>st. st = BlockedOnReceive x pl) t s; bound_tcb_at ((=) (Some ntfnptr)) t s; is_subject aag (cur_thread s); (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l t \<and> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> (\<forall>x. (\<exists>xa. st = BlockedOnReceive x xa) \<longrightarrow> aag_can_read_or_affect aag l x) \<and> (\<forall>x. (\<exists>xa. st = BlockedOnSend x xa) \<longrightarrow> aag_can_read_or_affect aag l x)) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>aag_can_read_or_affect aag l x; pas_refined aag s; is_subject aag (cur_thread s); (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag; kheap s t = Some (TCB tcb); tcb_state tcb = BlockedOnReceive x pl; Some ntfnptr = tcb_bound_notification tcb; aag_can_affect_label aag l \<longrightarrow> pasObjectAbs aag t \<notin> subjectReads (pasPolicy aag) l\<rbrakk> \<Longrightarrow> aag_can_read aag t proof (state)
this:
reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od)

goal (1 subgoal):
 1. \<not> aag_can_read_or_affect aag l x \<Longrightarrow> reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od) proof (state)
goal (1 subgoal):
 1. \<not> aag_can_read_or_affect aag l x \<Longrightarrow> reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od) proof (state)
this:
\<not> aag_can_read_or_affect aag l x

goal (1 subgoal):
 1. \<not> aag_can_read_or_affect aag l x \<Longrightarrow> reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od) proof (prove)
using this:
\<not> aag_can_read_or_affect aag l x

goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od) proof (prove)
goal (1 subgoal):
 1. \<not> aag_can_read_or_affect aag l x \<Longrightarrow> reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> aag_can_read_or_affect aag l x; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s))) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag; labels_are_invisible aag l {pasObjectAbs aag x}\<rbrakk> \<Longrightarrow> reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s))) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>labels_are_invisible aag l {pasObjectAbs aag x}; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s))) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue <- get_ep_queue ep;
return (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))
od >>= set_endpoint epptr
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>labels_are_invisible aag l {pasObjectAbs aag x}; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag x} (pas_refined aag and st_tcb_at (\<lambda>st. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s))) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue <- get_ep_queue ep;
return (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))
od >>= set_endpoint epptr
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>labels_are_invisible aag l {pasObjectAbs aag x}; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> modifies_at_most aag {pasObjectAbs aag x} (pas_refined aag and st_tcb_at (\<lambda>st. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s))) (do epptr <- do state <- get_thread_state t;
case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail
od;
do ep <- get_endpoint epptr;
queue <- get_ep_queue ep;
return (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))
od >>= set_endpoint epptr
od) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>labels_are_invisible aag l {pasObjectAbs aag x}; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and st_tcb_at (\<lambda>st. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and equiv_but_for_labels aag {pasObjectAbs aag x} st\<rbrace> do epptr <- do state <- get_thread_state t;
case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail
od;
do ep <- get_endpoint epptr;
queue <- get_ep_queue ep;
return (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))
od >>= set_endpoint epptr
od \<lbrace>\<lambda>_. equiv_but_for_labels aag {pasObjectAbs aag x} st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrakk>labels_are_invisible aag l {pasObjectAbs aag x}; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 st\<rbrace> do epptr <- do state <- get_thread_state t;
case state of BlockedOnReceive epptr x \<Rightarrow> return epptr | BlockedOnSend epptr x \<Rightarrow> return epptr | _ \<Rightarrow> fail
od;
do ep <- get_endpoint epptr;
queue <- get_ep_queue ep;
return (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))
od >>= set_endpoint epptr
od \<lbrace>\<lambda>_. equiv_but_for_labels aag {pasObjectAbs aag x} st\<rbrace>
 2. \<And>st s. \<lbrakk>labels_are_invisible aag l {pasObjectAbs aag x}; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag; (pas_refined aag and st_tcb_at (\<lambda>st. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and equiv_but_for_labels aag {pasObjectAbs aag x} st) s\<rbrakk> \<Longrightarrow> ?Q12 st s proof (prove)
goal (1 subgoal):
 1. \<And>st s sta. \<lbrakk>labels_are_invisible aag l {pasObjectAbs aag x}; (pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag; pas_refined aag s; st_tcb_at (\<lambda>st. st = BlockedOnReceive x pl) t s; bound_tcb_at ((=) (Some ntfnptr)) t s; is_subject aag (cur_thread s); equiv_but_for_labels aag {pasObjectAbs aag x} st s; st_tcb_at ((=) sta) t s\<rbrakk> \<Longrightarrow> (\<forall>xa. (\<exists>x. sta = BlockedOnReceive xa x) \<longrightarrow> pasObjectAbs aag xa = pasObjectAbs aag x) \<and> (\<forall>xa. (\<exists>x. sta = BlockedOnSend xa x) \<longrightarrow> pasObjectAbs aag xa = pasObjectAbs aag x) proof (state)
this:
reads_respects aag l (pas_refined aag and st_tcb_at (\<lambda>st. \<exists>xa. st = BlockedOnReceive x pl) t and bound_tcb_at ((=) (Some ntfnptr)) t and (\<lambda>s. is_subject aag (cur_thread s)) and K ((pasObjectAbs aag t, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag t, Receive, pasObjectAbs aag x) \<in> pasPolicy aag)) (do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od)

goal:
No subgoals! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do epptr <- get_thread_state t >>= get_blocking_object;
do ep <- get_endpoint epptr;
queue' <- do queue <- get_ep_queue ep;
return $ remove1 t queue
od;
return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep queue')
od >>= set_endpoint epptr
od \<lbrace>\<lambda>rv _. True\<rbrace>