theory Ipc_AC

lemma receive_ipc_pas_refined:
  "\<lbrace>pas_refined aag and invs and
    K (is_subject aag thread \<and> pas_cap_cur_auth aag ep_cap \<and> AllowRead \<in> cap_rights ep_cap)\<rbrace>
   receive_ipc thread ep_cap is_blocking
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: receive_ipc_def thread_get_def  split: cap.split) apply clarsimp apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) apply (rule hoare_seq_ext[OF _ gbn_sp]) apply (case_tac ntfnptr, simp_all) 
   (* old receive_ipc stuff *)
    apply (rule hoare_pre) apply (wp receive_ipc_base_pas_refined)[1] apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def) 
  (* ntfn-binding case *)
   apply clarsimp apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) apply (case_tac "isActive ntfn", simp_all) apply (wp complete_signal_pas_refined, clarsimp) apply fastforce 
  (* regular case again *)
   apply (rule hoare_pre, wp receive_ipc_base_pas_refined) apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and K (is_subject aag thread \<and> pas_cap_cur_auth aag ep_cap \<and> AllowRead \<in> cap_rights ep_cap)\<rbrace> receive_ipc thread ep_cap is_blocking \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag thread \<and> pas_cap_cur_auth aag ep_cap \<and> AllowRead \<in> cap_rights ep_cap \<Longrightarrow> \<lbrace>pas_refined aag and invs\<rbrace> receive_ipc thread ep_cap is_blocking \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag thread \<and> pas_cap_cur_auth aag ep_cap \<and> AllowRead \<in> cap_rights ep_cap \<Longrightarrow> \<forall>x31 x32 x33. ep_cap = EndpointCap x31 x32 x33 \<longrightarrow> \<lbrace>pas_refined aag and invs\<rbrace> do ep <- get_endpoint x31;
ntfnptr <- get_bound_notification thread;
ntfn <- case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x;
if (\<exists>y. ntfnptr = Some y) \<and> isActive ntfn then complete_signal (the ntfnptr) thread else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs\<rbrace> do ep <- get_endpoint x31;
ntfnptr <- get_bound_notification thread;
ntfn <- case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x;
if (\<exists>y. ntfnptr = Some y) \<and> isActive ntfn then complete_signal (the ntfnptr) thread else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 ep. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) x31 and (pas_refined aag and invs)\<rbrace> do ntfnptr <- get_bound_notification thread;
ntfn <- case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x;
if (\<exists>y. ntfnptr = Some y) \<and> isActive ntfn then complete_signal (the ntfnptr) thread else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 ep ntfnptr. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs))\<rbrace> do ntfn <- case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x;
if (\<exists>y. ntfnptr = Some y) \<and> isActive ntfn then complete_signal (the ntfnptr) thread else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 ep ntfnptr. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33; ntfnptr = None\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) None) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs))\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>x31 x32 x33 ep ntfnptr a. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33; ntfnptr = Some a\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) (Some a)) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs))\<rbrace> do ntfn <- get_notification a;
if isActive ntfn then complete_signal a thread else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 ep ntfnptr. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33; ntfnptr = None\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) None) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs))\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>x31 x32 x33 ep ntfnptr a. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33; ntfnptr = Some a\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) (Some a)) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs))\<rbrace> do ntfn <- get_notification a;
if isActive ntfn then complete_signal a thread else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 ep ntfnptr. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33; ntfnptr = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q26 x31 x32 x33 ep ntfnptr\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>x31 x32 x33 ep ntfnptr s. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33; ntfnptr = None; (bound_tcb_at ((=) None) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs))) s\<rbrakk> \<Longrightarrow> ?Q26 x31 x32 x33 ep ntfnptr s
 3. \<And>x31 x32 x33 ep ntfnptr a. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33; ntfnptr = Some a\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) (Some a)) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs))\<rbrace> do ntfn <- get_notification a;
if isActive ntfn then complete_signal a thread else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 ep ntfnptr s. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33; ntfnptr = None; (bound_tcb_at ((=) None) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs))) s\<rbrakk> \<Longrightarrow> (pas_refined aag and invs and ko_at (Endpoint ep) x31 and K (is_subject aag thread \<and> (pasSubject aag, Receive, pasObjectAbs aag x31) \<in> pasPolicy aag \<and> (\<forall>auth\<in>cap_rights_to_auth x33 True. (pasSubject aag, auth, pasObjectAbs aag x31) \<in> pasPolicy aag))) s
 2. \<And>x31 x32 x33 ep ntfnptr a. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33; ntfnptr = Some a\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) (Some a)) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs))\<rbrace> do ntfn <- get_notification a;
if isActive ntfn then complete_signal a thread else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 ep ntfnptr a. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33; ntfnptr = Some a\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) (Some a)) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs))\<rbrace> do ntfn <- get_notification a;
if isActive ntfn then complete_signal a thread else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 ep ntfnptr a. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33; ntfnptr = Some a\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) (Some a)) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs))\<rbrace> do ntfn <- get_notification a;
if isActive ntfn then complete_signal a thread else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 ep a. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) (Some a)) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs))\<rbrace> do ntfn <- get_notification a;
if isActive ntfn then complete_signal a thread else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 ep a ntfn. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification ntfn) a and (bound_tcb_at ((=) (Some a)) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs)))\<rbrace> if isActive ntfn then complete_signal a thread else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 ep a ntfn. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33; isActive ntfn\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification ntfn) a and (bound_tcb_at ((=) (Some a)) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs)))\<rbrace> complete_signal a thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>x31 x32 x33 ep a ntfn. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33; \<not> isActive ntfn\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification ntfn) a and (bound_tcb_at ((=) (Some a)) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs)))\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 ep a ntfn s. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33; isActive ntfn; ko_at (Notification ntfn) a s; bound_tcb_at ((=) (Some a)) thread s; ko_at (Endpoint ep) x31 s; pas_refined aag s; invs s\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s
 2. \<And>x31 x32 x33 ep a ntfn. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33; \<not> isActive ntfn\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification ntfn) a and (bound_tcb_at ((=) (Some a)) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs)))\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 ep a ntfn. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33; \<not> isActive ntfn\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification ntfn) a and (bound_tcb_at ((=) (Some a)) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs)))\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 ep a ntfn. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33; \<not> isActive ntfn\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification ntfn) a and (bound_tcb_at ((=) (Some a)) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs)))\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint x31 $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some x31) (sender_badge data) (sender_can_grant data) thread;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender thread (AllowGrant \<in> x33) else set_thread_state sender Inactive else do set_thread_state sender Running;
do_extended_op (possible_switch_to sender)
od
od | RecvEP queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 ep a ntfn s. \<lbrakk>is_subject aag thread; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; ep_cap = EndpointCap x31 x32 x33; \<not> isActive ntfn; (ko_at (Notification ntfn) a and (bound_tcb_at ((=) (Some a)) thread and (ko_at (Endpoint ep) x31 and (pas_refined aag and invs)))) s\<rbrakk> \<Longrightarrow> (pas_refined aag and invs and ko_at (Endpoint ep) x31 and K (is_subject aag thread \<and> (pasSubject aag, Receive, pasObjectAbs aag x31) \<in> pasPolicy aag \<and> (\<forall>auth\<in>cap_rights_to_auth x33 True. (pasSubject aag, auth, pasObjectAbs aag x31) \<in> pasPolicy aag))) s proof (prove)
goal:
No subgoals!