theory FinalCaps

lemma receive_ipc_silc_inv:
  "\<lbrace>silc_inv aag st and invs and pas_refined aag 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>_. silc_inv aag st\<rbrace>" unfolding receive_ipc_def apply (rule hoare_gen_asm) apply (simp del: AllowSend_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_silc_inv,
          clarsimp 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, clarsimp) 
   (* old receive case, bound ntfn not active *)
   apply (rule hoare_pre, wp receive_ipc_base_silc_inv,
         clarsimp 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>silc_inv aag st and invs and pas_refined aag 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>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and invs and pas_refined aag and K (is_subject aag receiver \<and> pas_cap_cur_auth aag cap \<and> AllowRead \<in> cap_rights cap)\<rbrace> do (epptr, rights) <- case cap of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail;
ep <- get_endpoint epptr;
ntfnptr <- get_bound_notification receiver;
ntfn <- case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x;
if ntfnptr \<noteq> None \<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 epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (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 epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref data \<Rightarrow> return data | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some epptr) (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> rights) 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 epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver
od \<lbrace>\<lambda>_. silc_inv aag 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>silc_inv aag st and invs and pas_refined aag\<rbrace> do (epptr, rights) <- case cap of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail;
ep <- get_endpoint epptr;
ntfnptr <- get_bound_notification receiver;
ntfn <- case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x;
if ntfnptr \<noteq> None \<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 epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (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 epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref data \<Rightarrow> return data | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some epptr) (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> rights) 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 epptr \<lparr>receiver_can_grant = AllowGrant \<in> rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [receiver]))
od | False \<Rightarrow> do_nbrecv_failed_transfer receiver
od \<lbrace>\<lambda>_. silc_inv aag 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>silc_inv aag st and invs and pas_refined aag\<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>_. silc_inv aag 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>silc_inv aag st and invs and pas_refined aag\<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>_. silc_inv aag 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 (silc_inv aag st and invs and pas_refined aag)\<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>_. silc_inv aag 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 (silc_inv aag st and invs and pas_refined aag))\<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>_. silc_inv aag 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 (silc_inv aag st and invs and pas_refined aag))\<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>_. silc_inv aag 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 (silc_inv aag st and invs and pas_refined aag))\<rbrace> do ntfn <- get_notification a;
if 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>_. silc_inv aag 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 (silc_inv aag st and invs and pas_refined aag))\<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>_. silc_inv aag 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 (silc_inv aag st and invs and pas_refined aag))\<rbrace> do ntfn <- get_notification a;
if 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>_. silc_inv aag 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 (silc_inv aag st and invs and pas_refined aag))\<rbrace> do ntfn <- get_notification a;
if 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>_. silc_inv aag 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 (silc_inv aag st and invs and pas_refined aag)))\<rbrace> if 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 \<lbrace>\<lambda>_. silc_inv aag 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 (silc_inv aag st and invs and pas_refined aag)))\<rbrace> complete_signal a receiver \<lbrace>\<lambda>_. silc_inv aag 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 (silc_inv aag st and invs and pas_refined aag)))\<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>_. silc_inv aag 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 (silc_inv aag st and invs and pas_refined aag)))\<rbrace> complete_signal a receiver \<lbrace>\<lambda>_. silc_inv aag 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 (silc_inv aag st and invs and pas_refined aag)))\<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>_. silc_inv aag 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 (silc_inv aag st and invs and pas_refined aag)))\<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>_. silc_inv aag 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 (silc_inv aag st and invs and pas_refined aag)))\<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>_. silc_inv aag st\<rbrace> proof (prove)
goal:
No subgoals!