theory Ipc_AC

lemma receive_ipc_integrity_autarch:
  "\<lbrace>pas_refined aag and integrity aag X st and invs and
    K (is_subject aag receiver \<and> pas_cap_cur_auth aag cap \<and> AllowRead \<in> cap_rights cap)\<rbrace>
   receive_ipc receiver cap is_blocking
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: receive_ipc_def split: cap.splits) 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 case, not bound *)
    apply (rule hoare_pre, wp receive_ipc_base_integrity) apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def) apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) apply (case_tac "isActive ntfn", simp_all) 
   (* new ntfn-binding case *)
    apply (rule hoare_pre, wp complete_signal_integrity, clarsimp) 
  (* old receive case, bound ntfn not active *)
   apply (rule hoare_pre, wp receive_ipc_base_integrity) 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 integrity aag X st and invs and K (is_subject aag receiver \<and> pas_cap_cur_auth aag cap \<and> AllowRead \<in> cap_rights cap)\<rbrace> receive_ipc receiver cap is_blocking \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag receiver \<and> pas_cap_cur_auth aag cap \<and> AllowRead \<in> cap_rights cap \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and invs\<rbrace> receive_ipc receiver cap is_blocking \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag receiver \<and> pas_cap_cur_auth aag cap \<and> AllowRead \<in> cap_rights cap \<Longrightarrow> \<forall>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and invs\<rbrace> do ep <- get_endpoint x31;
ntfnptr <- get_bound_notification receiver;
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) receiver else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | 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) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (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 receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and invs\<rbrace> do ep <- get_endpoint x31;
ntfnptr <- get_bound_notification receiver;
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) receiver else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | 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) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (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 receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 ep. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint ep) x31 and (pas_refined aag and integrity aag X st and invs)\<rbrace> do ntfnptr <- get_bound_notification receiver;
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) receiver else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | 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) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (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 receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 ep ntfnptr. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) receiver and (ko_at (Endpoint ep) x31 and (pas_refined aag and integrity aag X st 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) receiver else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | 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) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (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 receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 ep ntfnptr. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33; ntfnptr = None\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) None) receiver and (ko_at (Endpoint ep) x31 and (pas_refined aag and integrity aag X st and invs))\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | 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) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (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 receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>x31 x32 x33 ep ntfnptr a. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33; ntfnptr = Some a\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) (Some a)) receiver and (ko_at (Endpoint ep) x31 and (pas_refined aag and integrity aag X st and invs))\<rbrace> do ntfn <- get_notification a;
if isActive ntfn then complete_signal a receiver else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | 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) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (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 receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 ep ntfnptr. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33; ntfnptr = None\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) None) receiver and (ko_at (Endpoint ep) x31 and (pas_refined aag and integrity aag X st and invs))\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | 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) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (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 receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>x31 x32 x33 ep ntfnptr a. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33; ntfnptr = Some a\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) (Some a)) receiver and (ko_at (Endpoint ep) x31 and (pas_refined aag and integrity aag X st and invs))\<rbrace> do ntfn <- get_notification a;
if isActive ntfn then complete_signal a receiver else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | 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) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (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 receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 ep ntfnptr s. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33; ntfnptr = None; (bound_tcb_at ((=) None) receiver and (ko_at (Endpoint ep) x31 and (pas_refined aag and integrity aag X st and invs))) s\<rbrakk> \<Longrightarrow> (pas_refined aag and integrity aag X st and invs and ko_at (Endpoint ep) x31 and K (is_subject aag receiver \<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 receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33; ntfnptr = Some a\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) (Some a)) receiver and (ko_at (Endpoint ep) x31 and (pas_refined aag and integrity aag X st and invs))\<rbrace> do ntfn <- get_notification a;
if isActive ntfn then complete_signal a receiver else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | 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) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (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 receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 ep ntfnptr a. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33; ntfnptr = Some a\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) (Some a)) receiver and (ko_at (Endpoint ep) x31 and (pas_refined aag and integrity aag X st and invs))\<rbrace> do ntfn <- get_notification a;
if isActive ntfn then complete_signal a receiver else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | 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) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (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 receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 ep ntfnptr a ntfn. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33; ntfnptr = Some a\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification ntfn) a and (bound_tcb_at ((=) (Some a)) receiver and (ko_at (Endpoint ep) x31 and (pas_refined aag and integrity aag X st and invs)))\<rbrace> if isActive ntfn then complete_signal a receiver else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | 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) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (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 receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 ep ntfnptr a ntfn. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33; ntfnptr = Some a; isActive ntfn\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification ntfn) a and (bound_tcb_at ((=) (Some a)) receiver and (ko_at (Endpoint ep) x31 and (pas_refined aag and integrity aag X st and invs)))\<rbrace> complete_signal a receiver \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>x31 x32 x33 ep ntfnptr a ntfn. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33; ntfnptr = Some a; \<not> isActive ntfn\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification ntfn) a and (bound_tcb_at ((=) (Some a)) receiver and (ko_at (Endpoint ep) x31 and (pas_refined aag and integrity aag X st and invs)))\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | 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) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (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 receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 ep ntfnptr a ntfn. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33; ntfnptr = Some a; isActive ntfn\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification ntfn) a and (bound_tcb_at ((=) (Some a)) receiver and (ko_at (Endpoint ep) x31 and (pas_refined aag and integrity aag X st and invs)))\<rbrace> complete_signal a receiver \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>x31 x32 x33 ep ntfnptr a ntfn. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33; ntfnptr = Some a; \<not> isActive ntfn\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification ntfn) a and (bound_tcb_at ((=) (Some a)) receiver and (ko_at (Endpoint ep) x31 and (pas_refined aag and integrity aag X st and invs)))\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | 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) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (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 receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 ep ntfnptr a ntfn. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33; ntfnptr = Some a; \<not> isActive ntfn\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification ntfn) a and (bound_tcb_at ((=) (Some a)) receiver and (ko_at (Endpoint ep) x31 and (pas_refined aag and integrity aag X st and invs)))\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | 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) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (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 receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 ep ntfnptr a ntfn. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33; ntfnptr = Some a; \<not> isActive ntfn\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification ntfn) a and (bound_tcb_at ((=) (Some a)) receiver and (ko_at (Endpoint ep) x31 and (pas_refined aag and integrity aag X st and invs)))\<rbrace> case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP [receiver])
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver | 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) receiver;
if sender_is_call data then if sender_can_call data then setup_caller_cap sender receiver (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 receiver (BlockedOnReceive x31 \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint x31 (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 ep ntfnptr a ntfn s. \<lbrakk>is_subject aag receiver; pas_cap_cur_auth aag (EndpointCap x31 x32 x33); AllowRead \<in> x33; cap = EndpointCap x31 x32 x33; ntfnptr = Some a; \<not> isActive ntfn; (ko_at (Notification ntfn) a and (bound_tcb_at ((=) (Some a)) receiver and (ko_at (Endpoint ep) x31 and (pas_refined aag and integrity aag X st and invs)))) s\<rbrakk> \<Longrightarrow> (pas_refined aag and integrity aag X st and invs and ko_at (Endpoint ep) x31 and K (is_subject aag receiver \<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!