theory Ipc_DR

lemma recv_sync_ipc_corres:
  "\<lbrakk>epptr = cap_ep_ptr ep_cap; ep_id = epptr;  tcb_id_receiver = thread\<rbrakk>\<Longrightarrow>
    dcorres dc
     \<top>
     (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s)
      and st_tcb_at active thread
      and valid_state and valid_etcbs)
     (Endpoint_D.receive_ipc tcb_id_receiver ep_id (Grant \<in> cap_rights ep_cap))
     (Ipc_A.receive_ipc thread ep_cap is_blocking)" apply (clarsimp simp:corres_free_fail cap_ep_ptr_def Ipc_A.receive_ipc_def
                 split:cap.splits Structures_A.endpoint.splits) apply (rename_tac ep_badge ep_rights) apply (rule dcorres_expand_pfx) apply (rule_tac Q'="\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr" in corres_symb_exec_r) apply (simp add:Endpoint_D.receive_ipc_def get_bound_notification_def thread_get_def gets_the_def gets_def bind_assoc) apply (rule dcorres_absorb_get_r) apply (clarsimp simp: assert_opt_def corres_free_fail split: Structures_A.kernel_object.splits option.splits ) apply safe[1]
     \<comment> \<open>not bound\<close> apply (rule corres_alternate2) apply (rule dcorres_receive_sync, simp_all)[1] apply (simp add: get_simple_ko_def gets_def get_object_def bind_assoc) apply (rule dcorres_absorb_get_r) apply (frule get_tcb_SomeD) apply (clarsimp simp add: valid_state_def valid_pspace_def
                     split: kernel_object.splits if_splits) apply (rule valid_objsE, assumption, simp) apply (clarsimp simp: valid_obj_def valid_tcb_def valid_bound_ntfn_def) apply (clarsimp simp: assert_def corres_free_fail obj_at_def partial_inv_def
                    split: Structures_A.kernel_object.splits) apply safe[1] apply (rule corres_alternate1) apply (rule corres_guard_imp) apply (rule dcorres_complete_signal, simp+) apply (rule corres_alternate2) apply (rule dcorres_receive_sync, simp_all add: obj_at_def valid_state_def valid_pspace_def)[1] apply (wp get_simple_ko_ko_at | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>epptr = cap_ep_ptr ep_cap; ep_id = epptr; tcb_id_receiver = thread\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) (Endpoint_D.receive_ipc tcb_id_receiver ep_id (AllowGrant \<in> Structures_A.cap_rights ep_cap)) (Ipc_A.receive_ipc thread ep_cap is_blocking) proof (prove)
goal (1 subgoal):
 1. \<And>x32 x33. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr x32 x33\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) (Endpoint_D.receive_ipc thread epptr (AllowGrant \<in> x33)) (do ep <- get_endpoint epptr;
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 epptr \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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 epptr \<lparr>receiver_can_grant = AllowGrant \<in> x33\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od) proof (prove)
goal (1 subgoal):
 1. \<And>ep_badge ep_rights. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) (Endpoint_D.receive_ipc thread epptr (AllowGrant \<in> ep_rights)) (do ep <- get_endpoint epptr;
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 epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od) proof (prove)
goal (1 subgoal):
 1. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (Endpoint_D.receive_ipc thread epptr (AllowGrant \<in> ep_rights)) (do ep <- get_endpoint epptr;
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 epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od) proof (prove)
goal (4 subgoals):
 1. \<And>ep_badge ep_rights s s' rv. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s' and ko_at (kernel_object.Endpoint rv) epptr) (Endpoint_D.receive_ipc thread epptr (AllowGrant \<in> ep_rights)) (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 rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od)
 2. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 3. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (4 subgoals):
 1. \<And>ep_badge ep_rights s s' rv. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; ep_at epptr s' \<and> not_idle_thread thread s' \<and> not_idle_thread (cur_thread s') s' \<and> st_tcb_at active thread s' \<and> valid_state s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s' and ko_at (kernel_object.Endpoint rv) epptr) (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (do x <- get;
tcb <- assert_opt (get_tcb thread x);
ntfn <- case tcb_bound_notification tcb of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x;
if (\<exists>y. tcb_bound_notification tcb = Some y) \<and> isActive ntfn then complete_signal (the (tcb_bound_notification tcb)) thread else case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od)
 2. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 3. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (4 subgoals):
 1. \<And>ep_badge ep_rights s s' rv s'a. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; ep_at epptr s' \<and> not_idle_thread thread s' \<and> not_idle_thread (cur_thread s') s' \<and> st_tcb_at active thread s' \<and> valid_state s' \<and> valid_etcbs s'; transform s' = transform s'a; ((=) s' and ko_at (kernel_object.Endpoint rv) epptr) s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (do tcb <- assert_opt (get_tcb thread s'a);
ntfn <- case tcb_bound_notification tcb of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x;
if (\<exists>y. tcb_bound_notification tcb = Some y) \<and> isActive ntfn then complete_signal (the (tcb_bound_notification tcb)) thread else case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od)
 2. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 3. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (4 subgoals):
 1. \<And>ep_badge ep_rights s' rv x2. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; ko_at (kernel_object.Endpoint rv) epptr s'; ep_at epptr s'; not_idle_thread thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active thread s'; valid_state s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (tcb_bound_notification x2 = None \<longrightarrow> get_tcb thread s' = Some x2 \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)) \<and> (\<forall>x2a. tcb_bound_notification x2 = Some x2a \<longrightarrow> get_tcb thread s' = Some x2 \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (do ntfn <- get_notification x2a;
if isActive ntfn then complete_signal (the (tcb_bound_notification x2)) thread else case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od))
 2. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 3. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (5 subgoals):
 1. \<And>ep_badge ep_rights s' rv x2. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; ko_at (kernel_object.Endpoint rv) epptr s'; ep_at epptr s'; not_idle_thread thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active thread s'; valid_state s'; valid_etcbs s'; tcb_bound_notification x2 = None; get_tcb thread s' = Some x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 2. \<And>ep_badge ep_rights s' rv x2 x2a. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; ko_at (kernel_object.Endpoint rv) epptr s'; ep_at epptr s'; not_idle_thread thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active thread s'; valid_state s'; valid_etcbs s'; tcb_bound_notification x2 = Some x2a; get_tcb thread s' = Some x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (do ntfn <- get_notification x2a;
if isActive ntfn then complete_signal (the (tcb_bound_notification x2)) thread else case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od)
 3. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 4. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (5 subgoals):
 1. \<And>ep_badge ep_rights s' rv x2. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; ko_at (kernel_object.Endpoint rv) epptr s'; ep_at epptr s'; not_idle_thread thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active thread s'; valid_state s'; valid_etcbs s'; tcb_bound_notification x2 = None; get_tcb thread s' = Some x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (receive_sync thread epptr (AllowGrant \<in> ep_rights)) (case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 2. \<And>ep_badge ep_rights s' rv x2 x2a. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; ko_at (kernel_object.Endpoint rv) epptr s'; ep_at epptr s'; not_idle_thread thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active thread s'; valid_state s'; valid_etcbs s'; tcb_bound_notification x2 = Some x2a; get_tcb thread s' = Some x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (do ntfn <- get_notification x2a;
if isActive ntfn then complete_signal (the (tcb_bound_notification x2)) thread else case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od)
 3. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 4. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (4 subgoals):
 1. \<And>ep_badge ep_rights s' rv x2 x2a. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; ko_at (kernel_object.Endpoint rv) epptr s'; ep_at epptr s'; not_idle_thread thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active thread s'; valid_state s'; valid_etcbs s'; tcb_bound_notification x2 = Some x2a; get_tcb thread s' = Some x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (do ntfn <- get_notification x2a;
if isActive ntfn then complete_signal (the (tcb_bound_notification x2)) thread else case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od)
 2. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 3. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (4 subgoals):
 1. \<And>ep_badge ep_rights s' rv x2 x2a. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; ko_at (kernel_object.Endpoint rv) epptr s'; ep_at epptr s'; not_idle_thread thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active thread s'; valid_state s'; valid_etcbs s'; tcb_bound_notification x2 = Some x2a; get_tcb thread s' = Some x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (do x <- get;
xa <- assert (\<exists>y. kheap x x2a = Some y);
xa <- assert (a_type (the (kheap x x2a)) = AEndpoint \<or> a_type (the (kheap x x2a)) = ANTFN);
ntfn <- case partial_inv kernel_object.Notification (the (kheap x x2a)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
if isActive ntfn then complete_signal (the (tcb_bound_notification x2)) thread else case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od)
 2. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 3. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (4 subgoals):
 1. \<And>ep_badge ep_rights s' rv x2 x2a s'a. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; ko_at (kernel_object.Endpoint rv) epptr s'; ep_at epptr s'; not_idle_thread thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active thread s'; valid_state s'; valid_etcbs s'; tcb_bound_notification x2 = Some x2a; get_tcb thread s' = Some x2; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (do x <- assert (\<exists>y. kheap s'a x2a = Some y);
x <- assert (a_type (the (kheap s'a x2a)) = AEndpoint \<or> a_type (the (kheap s'a x2a)) = ANTFN);
ntfn <- case partial_inv kernel_object.Notification (the (kheap s'a x2a)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
if isActive ntfn then complete_signal (the (tcb_bound_notification x2)) thread else case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od)
 2. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 3. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (4 subgoals):
 1. \<And>ep_badge ep_rights s' rv x2 x2a s'a. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; ko_at (kernel_object.Endpoint rv) epptr s'; ep_at epptr s'; not_idle_thread thread s'; not_idle_thread (cur_thread s') s'; st_tcb_at active thread s'; valid_state s'; valid_etcbs s'; tcb_bound_notification x2 = Some x2a; get_tcb thread s' = Some x2; transform s' = transform s'a; s' = s'a; kheap s' thread = Some (TCB x2)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (do x <- assert (\<exists>y. kheap s'a x2a = Some y);
x <- assert (a_type (the (kheap s'a x2a)) = AEndpoint \<or> a_type (the (kheap s'a x2a)) = ANTFN);
ntfn <- case partial_inv kernel_object.Notification (the (kheap s'a x2a)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
if isActive ntfn then complete_signal (the (tcb_bound_notification x2)) thread else case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od)
 2. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 3. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (4 subgoals):
 1. \<And>ep_badge ep_rights rv x2 x2a s'a. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; ko_at (kernel_object.Endpoint rv) epptr s'a; ep_at epptr s'a; not_idle_thread thread s'a; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'a; valid_etcbs s'a; tcb_bound_notification x2 = Some x2a; get_tcb thread s'a = Some x2; kheap s'a thread = Some (TCB x2); valid_objs s'a; pspace_aligned s'a; pspace_distinct s'a; if_live_then_nonz_cap s'a; zombies_final s'a; sym_refs (state_refs_of s'a); sym_refs (state_hyp_refs_of s'a); valid_mdb s'a; valid_ioc s'a; valid_idle s'a; only_idle s'a; if_unsafe_then_cap s'a; valid_reply_caps s'a; valid_reply_masters s'a; valid_global_refs s'a; valid_arch_state s'a; valid_irq_node s'a; valid_irq_handlers s'a; valid_irq_states s'a; valid_machine_state s'a; valid_vspace_objs s'a; valid_arch_caps s'a; valid_global_objs s'a; valid_kernel_mappings s'a; equal_kernel_mappings s'a; valid_asid_map s'a; valid_global_vspace_mappings s'a; pspace_in_kernel_window s'a; cap_refs_in_kernel_window s'a; pspace_respects_device_region s'a; cap_refs_respects_device_region s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (do x <- assert (\<exists>y. kheap s'a x2a = Some y);
x <- assert (a_type (the (kheap s'a x2a)) = AEndpoint \<or> a_type (the (kheap s'a x2a)) = ANTFN);
ntfn <- case partial_inv kernel_object.Notification (the (kheap s'a x2a)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
if isActive ntfn then complete_signal (the (tcb_bound_notification x2)) thread else case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od)
 2. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 3. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (4 subgoals):
 1. \<And>ep_badge ep_rights rv x2 x2a s'a. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; ko_at (kernel_object.Endpoint rv) epptr s'a; ep_at epptr s'a; not_idle_thread thread s'a; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'a; valid_etcbs s'a; tcb_bound_notification x2 = Some x2a; get_tcb thread s'a = Some x2; kheap s'a thread = Some (TCB x2); valid_objs s'a; pspace_aligned s'a; pspace_distinct s'a; if_live_then_nonz_cap s'a; zombies_final s'a; sym_refs (state_refs_of s'a); sym_refs (state_hyp_refs_of s'a); valid_mdb s'a; valid_ioc s'a; valid_idle s'a; only_idle s'a; if_unsafe_then_cap s'a; valid_reply_caps s'a; valid_reply_masters s'a; valid_global_refs s'a; valid_arch_state s'a; valid_irq_node s'a; valid_irq_handlers s'a; valid_irq_states s'a; valid_machine_state s'a; valid_vspace_objs s'a; valid_arch_caps s'a; valid_global_objs s'a; valid_kernel_mappings s'a; equal_kernel_mappings s'a; valid_asid_map s'a; valid_global_vspace_mappings s'a; pspace_in_kernel_window s'a; cap_refs_in_kernel_window s'a; pspace_respects_device_region s'a; cap_refs_respects_device_region s'a; valid_obj thread (TCB x2) s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (do x <- assert (\<exists>y. kheap s'a x2a = Some y);
x <- assert (a_type (the (kheap s'a x2a)) = AEndpoint \<or> a_type (the (kheap s'a x2a)) = ANTFN);
ntfn <- case partial_inv kernel_object.Notification (the (kheap s'a x2a)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
if isActive ntfn then complete_signal (the (tcb_bound_notification x2)) thread else case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od)
 2. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 3. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (4 subgoals):
 1. \<And>ep_badge ep_rights rv x2 x2a s'a. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; ko_at (kernel_object.Endpoint rv) epptr s'a; ep_at epptr s'a; not_idle_thread thread s'a; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'a; valid_etcbs s'a; tcb_bound_notification x2 = Some x2a; get_tcb thread s'a = Some x2; kheap s'a thread = Some (TCB x2); valid_objs s'a; pspace_aligned s'a; pspace_distinct s'a; if_live_then_nonz_cap s'a; zombies_final s'a; sym_refs (state_refs_of s'a); sym_refs (state_hyp_refs_of s'a); valid_mdb s'a; valid_ioc s'a; valid_idle s'a; only_idle s'a; if_unsafe_then_cap s'a; valid_reply_caps s'a; valid_reply_masters s'a; valid_global_refs s'a; valid_arch_state s'a; valid_irq_node s'a; valid_irq_handlers s'a; valid_irq_states s'a; valid_machine_state s'a; valid_vspace_objs s'a; valid_arch_caps s'a; valid_global_objs s'a; valid_kernel_mappings s'a; equal_kernel_mappings s'a; valid_asid_map s'a; valid_global_vspace_mappings s'a; pspace_in_kernel_window s'a; cap_refs_in_kernel_window s'a; pspace_respects_device_region s'a; cap_refs_respects_device_region s'a; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s'a \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr thread (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s'a; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; ntfn_at x2a s'a; valid_arch_tcb (tcb_arch x2) s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (do x <- assert (\<exists>y. kheap s'a x2a = Some y);
x <- assert (a_type (the (kheap s'a x2a)) = AEndpoint \<or> a_type (the (kheap s'a x2a)) = ANTFN);
ntfn <- case partial_inv kernel_object.Notification (the (kheap s'a x2a)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
if isActive ntfn then complete_signal (the (tcb_bound_notification x2)) thread else case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread
od)
 2. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 3. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (4 subgoals):
 1. \<And>ep_badge ep_rights rv x2 x2a s'a ko. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; kheap s'a epptr = Some (kernel_object.Endpoint rv); is_ep (kernel_object.Endpoint rv); not_idle_thread thread s'a; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'a; valid_etcbs s'a; tcb_bound_notification x2 = Some x2a; get_tcb thread s'a = Some x2; kheap s'a thread = Some (TCB x2); valid_objs s'a; pspace_aligned s'a; pspace_distinct s'a; if_live_then_nonz_cap s'a; zombies_final s'a; sym_refs (state_refs_of s'a); sym_refs (state_hyp_refs_of s'a); valid_mdb s'a; valid_ioc s'a; valid_idle s'a; only_idle s'a; if_unsafe_then_cap s'a; valid_reply_caps s'a; valid_reply_masters s'a; valid_global_refs s'a; valid_arch_state s'a; valid_irq_node s'a; valid_irq_handlers s'a; valid_irq_states s'a; valid_machine_state s'a; valid_vspace_objs s'a; valid_arch_caps s'a; valid_global_objs s'a; valid_kernel_mappings s'a; equal_kernel_mappings s'a; valid_asid_map s'a; valid_global_vspace_mappings s'a; pspace_in_kernel_window s'a; cap_refs_in_kernel_window s'a; pspace_respects_device_region s'a; cap_refs_respects_device_region s'a; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s'a \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr thread (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s'a; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_arch_tcb (tcb_arch x2) s'a; kheap s'a x2a = Some ko; is_ntfn ko\<rbrakk> \<Longrightarrow> (isActive (THE y. kernel_object.Notification y = ko) \<longrightarrow> (\<exists>!y. kernel_object.Notification y = ko) \<longrightarrow> (a_type ko = AEndpoint \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (complete_signal x2a thread)) \<and> (a_type ko = ANTFN \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (complete_signal x2a thread))) \<and> (\<not> isActive (THE y. kernel_object.Notification y = ko) \<longrightarrow> (\<exists>!y. kernel_object.Notification y = ko) \<longrightarrow> (a_type ko = AEndpoint \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)) \<and> (a_type ko = ANTFN \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)))
 2. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 3. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (5 subgoals):
 1. \<And>ep_badge ep_rights rv x2 x2a s'a ko y ntfn. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; kheap s'a epptr = Some (kernel_object.Endpoint rv); is_ep (kernel_object.Endpoint rv); not_idle_thread thread s'a; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'a; valid_etcbs s'a; tcb_bound_notification x2 = Some x2a; get_tcb thread s'a = Some x2; kheap s'a thread = Some (TCB x2); valid_objs s'a; pspace_aligned s'a; pspace_distinct s'a; if_live_then_nonz_cap s'a; zombies_final s'a; sym_refs (state_refs_of s'a); sym_refs (state_hyp_refs_of s'a); valid_mdb s'a; valid_ioc s'a; valid_idle s'a; only_idle s'a; if_unsafe_then_cap s'a; valid_reply_caps s'a; valid_reply_masters s'a; valid_global_refs s'a; valid_arch_state s'a; valid_irq_node s'a; valid_irq_handlers s'a; valid_irq_states s'a; valid_machine_state s'a; valid_vspace_objs s'a; valid_arch_caps s'a; valid_global_objs s'a; valid_kernel_mappings s'a; equal_kernel_mappings s'a; valid_asid_map s'a; valid_global_vspace_mappings s'a; pspace_in_kernel_window s'a; cap_refs_in_kernel_window s'a; pspace_respects_device_region s'a; cap_refs_respects_device_region s'a; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s'a \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr thread (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s'a; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_arch_tcb (tcb_arch x2) s'a; kheap s'a x2a = Some (kernel_object.Notification ntfn); is_ntfn (kernel_object.Notification ntfn); isActive (THE y. kernel_object.Notification y = kernel_object.Notification ntfn); \<forall>y y'. kernel_object.Notification y = kernel_object.Notification ntfn \<and> kernel_object.Notification y' = kernel_object.Notification ntfn \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (complete_signal x2a thread)
 2. \<And>ep_badge ep_rights rv x2 x2a s'a ko y ntfn. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; kheap s'a epptr = Some (kernel_object.Endpoint rv); is_ep (kernel_object.Endpoint rv); not_idle_thread thread s'a; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'a; valid_etcbs s'a; tcb_bound_notification x2 = Some x2a; get_tcb thread s'a = Some x2; kheap s'a thread = Some (TCB x2); valid_objs s'a; pspace_aligned s'a; pspace_distinct s'a; if_live_then_nonz_cap s'a; zombies_final s'a; sym_refs (state_refs_of s'a); sym_refs (state_hyp_refs_of s'a); valid_mdb s'a; valid_ioc s'a; valid_idle s'a; only_idle s'a; if_unsafe_then_cap s'a; valid_reply_caps s'a; valid_reply_masters s'a; valid_global_refs s'a; valid_arch_state s'a; valid_irq_node s'a; valid_irq_handlers s'a; valid_irq_states s'a; valid_machine_state s'a; valid_vspace_objs s'a; valid_arch_caps s'a; valid_global_objs s'a; valid_kernel_mappings s'a; equal_kernel_mappings s'a; valid_asid_map s'a; valid_global_vspace_mappings s'a; pspace_in_kernel_window s'a; cap_refs_in_kernel_window s'a; pspace_respects_device_region s'a; cap_refs_respects_device_region s'a; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s'a \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr thread (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s'a; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_arch_tcb (tcb_arch x2) s'a; kheap s'a x2a = Some (kernel_object.Notification ntfn); is_ntfn (kernel_object.Notification ntfn); \<not> isActive (THE y. kernel_object.Notification y = kernel_object.Notification ntfn); \<forall>y y'. kernel_object.Notification y = kernel_object.Notification ntfn \<and> kernel_object.Notification y' = kernel_object.Notification ntfn \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 3. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 4. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (5 subgoals):
 1. \<And>ep_badge ep_rights rv x2 x2a s'a ko y ntfn. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; kheap s'a epptr = Some (kernel_object.Endpoint rv); is_ep (kernel_object.Endpoint rv); not_idle_thread thread s'a; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'a; valid_etcbs s'a; tcb_bound_notification x2 = Some x2a; get_tcb thread s'a = Some x2; kheap s'a thread = Some (TCB x2); valid_objs s'a; pspace_aligned s'a; pspace_distinct s'a; if_live_then_nonz_cap s'a; zombies_final s'a; sym_refs (state_refs_of s'a); sym_refs (state_hyp_refs_of s'a); valid_mdb s'a; valid_ioc s'a; valid_idle s'a; only_idle s'a; if_unsafe_then_cap s'a; valid_reply_caps s'a; valid_reply_masters s'a; valid_global_refs s'a; valid_arch_state s'a; valid_irq_node s'a; valid_irq_handlers s'a; valid_irq_states s'a; valid_machine_state s'a; valid_vspace_objs s'a; valid_arch_caps s'a; valid_global_objs s'a; valid_kernel_mappings s'a; equal_kernel_mappings s'a; valid_asid_map s'a; valid_global_vspace_mappings s'a; pspace_in_kernel_window s'a; cap_refs_in_kernel_window s'a; pspace_respects_device_region s'a; cap_refs_respects_device_region s'a; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s'a \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr thread (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s'a; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_arch_tcb (tcb_arch x2) s'a; kheap s'a x2a = Some (kernel_object.Notification ntfn); is_ntfn (kernel_object.Notification ntfn); isActive (THE y. kernel_object.Notification y = kernel_object.Notification ntfn); \<forall>y y'. kernel_object.Notification y = kernel_object.Notification ntfn \<and> kernel_object.Notification y' = kernel_object.Notification ntfn \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent thread) (complete_signal x2a thread)
 2. \<And>ep_badge ep_rights rv x2 x2a s'a ko y ntfn. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; kheap s'a epptr = Some (kernel_object.Endpoint rv); is_ep (kernel_object.Endpoint rv); not_idle_thread thread s'a; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'a; valid_etcbs s'a; tcb_bound_notification x2 = Some x2a; get_tcb thread s'a = Some x2; kheap s'a thread = Some (TCB x2); valid_objs s'a; pspace_aligned s'a; pspace_distinct s'a; if_live_then_nonz_cap s'a; zombies_final s'a; sym_refs (state_refs_of s'a); sym_refs (state_hyp_refs_of s'a); valid_mdb s'a; valid_ioc s'a; valid_idle s'a; only_idle s'a; if_unsafe_then_cap s'a; valid_reply_caps s'a; valid_reply_masters s'a; valid_global_refs s'a; valid_arch_state s'a; valid_irq_node s'a; valid_irq_handlers s'a; valid_irq_states s'a; valid_machine_state s'a; valid_vspace_objs s'a; valid_arch_caps s'a; valid_global_objs s'a; valid_kernel_mappings s'a; equal_kernel_mappings s'a; valid_asid_map s'a; valid_global_vspace_mappings s'a; pspace_in_kernel_window s'a; cap_refs_in_kernel_window s'a; pspace_respects_device_region s'a; cap_refs_respects_device_region s'a; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s'a \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr thread (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s'a; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_arch_tcb (tcb_arch x2) s'a; kheap s'a x2a = Some (kernel_object.Notification ntfn); is_ntfn (kernel_object.Notification ntfn); \<not> isActive (THE y. kernel_object.Notification y = kernel_object.Notification ntfn); \<forall>y y'. kernel_object.Notification y = kernel_object.Notification ntfn \<and> kernel_object.Notification y' = kernel_object.Notification ntfn \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 3. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 4. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (7 subgoals):
 1. \<And>ep_badge ep_rights rv x2 x2a s'a ko y ntfn. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; kheap s'a epptr = Some (kernel_object.Endpoint rv); is_ep (kernel_object.Endpoint rv); not_idle_thread thread s'a; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'a; valid_etcbs s'a; tcb_bound_notification x2 = Some x2a; get_tcb thread s'a = Some x2; kheap s'a thread = Some (TCB x2); valid_objs s'a; pspace_aligned s'a; pspace_distinct s'a; if_live_then_nonz_cap s'a; zombies_final s'a; sym_refs (state_refs_of s'a); sym_refs (state_hyp_refs_of s'a); valid_mdb s'a; valid_ioc s'a; valid_idle s'a; only_idle s'a; if_unsafe_then_cap s'a; valid_reply_caps s'a; valid_reply_masters s'a; valid_global_refs s'a; valid_arch_state s'a; valid_irq_node s'a; valid_irq_handlers s'a; valid_irq_states s'a; valid_machine_state s'a; valid_vspace_objs s'a; valid_arch_caps s'a; valid_global_objs s'a; valid_kernel_mappings s'a; equal_kernel_mappings s'a; valid_asid_map s'a; valid_global_vspace_mappings s'a; pspace_in_kernel_window s'a; cap_refs_in_kernel_window s'a; pspace_respects_device_region s'a; cap_refs_respects_device_region s'a; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s'a \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr thread (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s'a; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_arch_tcb (tcb_arch x2) s'a; kheap s'a x2a = Some (kernel_object.Notification ntfn); is_ntfn (kernel_object.Notification ntfn); isActive (THE y. kernel_object.Notification y = kernel_object.Notification ntfn); \<forall>y y'. kernel_object.Notification y = kernel_object.Notification ntfn \<and> kernel_object.Notification y' = kernel_object.Notification ntfn \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> dcorres dc (?Q156 ep_badge ep_rights rv x2 x2a s'a ko y ntfn) (?Q'156 ep_badge ep_rights rv x2 x2a s'a ko y ntfn) (corrupt_tcb_intent thread) (complete_signal x2a thread)
 2. \<And>ep_badge ep_rights rv x2 x2a s'a ko y ntfn s. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; kheap s'a epptr = Some (kernel_object.Endpoint rv); is_ep (kernel_object.Endpoint rv); not_idle_thread thread s'a; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'a; valid_etcbs s'a; tcb_bound_notification x2 = Some x2a; get_tcb thread s'a = Some x2; kheap s'a thread = Some (TCB x2); valid_objs s'a; pspace_aligned s'a; pspace_distinct s'a; if_live_then_nonz_cap s'a; zombies_final s'a; sym_refs (state_refs_of s'a); sym_refs (state_hyp_refs_of s'a); valid_mdb s'a; valid_ioc s'a; valid_idle s'a; only_idle s'a; if_unsafe_then_cap s'a; valid_reply_caps s'a; valid_reply_masters s'a; valid_global_refs s'a; valid_arch_state s'a; valid_irq_node s'a; valid_irq_handlers s'a; valid_irq_states s'a; valid_machine_state s'a; valid_vspace_objs s'a; valid_arch_caps s'a; valid_global_objs s'a; valid_kernel_mappings s'a; equal_kernel_mappings s'a; valid_asid_map s'a; valid_global_vspace_mappings s'a; pspace_in_kernel_window s'a; cap_refs_in_kernel_window s'a; pspace_respects_device_region s'a; cap_refs_respects_device_region s'a; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s'a \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr thread (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s'a; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_arch_tcb (tcb_arch x2) s'a; kheap s'a x2a = Some (kernel_object.Notification ntfn); is_ntfn (kernel_object.Notification ntfn); isActive (THE y. kernel_object.Notification y = kernel_object.Notification ntfn); \<forall>y y'. kernel_object.Notification y = kernel_object.Notification ntfn \<and> kernel_object.Notification y' = kernel_object.Notification ntfn \<longrightarrow> y = y'; transform s'a = s\<rbrakk> \<Longrightarrow> ?Q156 ep_badge ep_rights rv x2 x2a s'a ko y ntfn s
 3. \<And>ep_badge ep_rights rv x2 x2a s'a ko y ntfn s. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; kheap s'a epptr = Some (kernel_object.Endpoint rv); is_ep (kernel_object.Endpoint rv); not_idle_thread thread s'a; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'a; valid_etcbs s'a; tcb_bound_notification x2 = Some x2a; get_tcb thread s'a = Some x2; kheap s'a thread = Some (TCB x2); valid_objs s'a; pspace_aligned s'a; pspace_distinct s'a; if_live_then_nonz_cap s'a; zombies_final s'a; sym_refs (state_refs_of s'a); sym_refs (state_hyp_refs_of s'a); valid_mdb s'a; valid_ioc s'a; valid_idle s'a; only_idle s'a; if_unsafe_then_cap s'a; valid_reply_caps s'a; valid_reply_masters s'a; valid_global_refs s'a; valid_arch_state s'a; valid_irq_node s'a; valid_irq_handlers s'a; valid_irq_states s'a; valid_machine_state s'a; valid_vspace_objs s'a; valid_arch_caps s'a; valid_global_objs s'a; valid_kernel_mappings s'a; equal_kernel_mappings s'a; valid_asid_map s'a; valid_global_vspace_mappings s'a; pspace_in_kernel_window s'a; cap_refs_in_kernel_window s'a; pspace_respects_device_region s'a; cap_refs_respects_device_region s'a; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s'a \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr thread (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s'a; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_arch_tcb (tcb_arch x2) s'a; kheap s'a x2a = Some (kernel_object.Notification ntfn); is_ntfn (kernel_object.Notification ntfn); isActive (THE y. kernel_object.Notification y = kernel_object.Notification ntfn); \<forall>y y'. kernel_object.Notification y = kernel_object.Notification ntfn \<and> kernel_object.Notification y' = kernel_object.Notification ntfn \<longrightarrow> y = y'; s'a = s\<rbrakk> \<Longrightarrow> ?Q'156 ep_badge ep_rights rv x2 x2a s'a ko y ntfn s
 4. \<And>ep_badge ep_rights rv x2 x2a s'a ko y ntfn. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; kheap s'a epptr = Some (kernel_object.Endpoint rv); is_ep (kernel_object.Endpoint rv); not_idle_thread thread s'a; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'a; valid_etcbs s'a; tcb_bound_notification x2 = Some x2a; get_tcb thread s'a = Some x2; kheap s'a thread = Some (TCB x2); valid_objs s'a; pspace_aligned s'a; pspace_distinct s'a; if_live_then_nonz_cap s'a; zombies_final s'a; sym_refs (state_refs_of s'a); sym_refs (state_hyp_refs_of s'a); valid_mdb s'a; valid_ioc s'a; valid_idle s'a; only_idle s'a; if_unsafe_then_cap s'a; valid_reply_caps s'a; valid_reply_masters s'a; valid_global_refs s'a; valid_arch_state s'a; valid_irq_node s'a; valid_irq_handlers s'a; valid_irq_states s'a; valid_machine_state s'a; valid_vspace_objs s'a; valid_arch_caps s'a; valid_global_objs s'a; valid_kernel_mappings s'a; equal_kernel_mappings s'a; valid_asid_map s'a; valid_global_vspace_mappings s'a; pspace_in_kernel_window s'a; cap_refs_in_kernel_window s'a; pspace_respects_device_region s'a; cap_refs_respects_device_region s'a; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s'a \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr thread (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s'a; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; valid_arch_tcb (tcb_arch x2) s'a; kheap s'a x2a = Some (kernel_object.Notification ntfn); is_ntfn (kernel_object.Notification ntfn); \<not> isActive (THE y. kernel_object.Notification y = kernel_object.Notification ntfn); \<forall>y y'. kernel_object.Notification y = kernel_object.Notification ntfn \<and> kernel_object.Notification y' = kernel_object.Notification ntfn \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 5. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 6. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 7. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (4 subgoals):
 1. \<And>ep_badge ep_rights rv x2 x2a s'a ntfn. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; kheap s'a epptr = Some (kernel_object.Endpoint rv); is_ep (kernel_object.Endpoint rv); not_idle_thread thread s'a; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'a; valid_etcbs s'a; tcb_bound_notification x2 = Some x2a; get_tcb thread s'a = Some x2; kheap s'a thread = Some (TCB x2); valid_objs s'a; pspace_aligned s'a; pspace_distinct s'a; if_live_then_nonz_cap s'a; zombies_final s'a; sym_refs (state_refs_of s'a); sym_refs (state_hyp_refs_of s'a); valid_mdb s'a; valid_ioc s'a; valid_idle s'a; only_idle s'a; if_unsafe_then_cap s'a; valid_reply_caps s'a; valid_reply_masters s'a; valid_global_refs s'a; valid_arch_state s'a; valid_irq_node s'a; valid_irq_handlers s'a; valid_irq_states s'a; valid_machine_state s'a; valid_vspace_objs s'a; valid_arch_caps s'a; valid_global_objs s'a; valid_kernel_mappings s'a; equal_kernel_mappings s'a; valid_asid_map s'a; valid_global_vspace_mappings s'a; pspace_in_kernel_window s'a; cap_refs_in_kernel_window s'a; pspace_respects_device_region s'a; cap_refs_respects_device_region s'a; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s'a \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr thread (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s'a; case tcb_fault x2 of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler x2) = word_bits; valid_arch_tcb (tcb_arch x2) s'a; kheap s'a x2a = Some (kernel_object.Notification ntfn); is_ntfn (kernel_object.Notification ntfn); \<not> isActive ntfn\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent thread \<sqinter> receive_sync thread epptr (AllowGrant \<in> ep_rights)) (case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 2. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 3. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (4 subgoals):
 1. \<And>ep_badge ep_rights rv x2 x2a s'a ntfn. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; kheap s'a epptr = Some (kernel_object.Endpoint rv); is_ep (kernel_object.Endpoint rv); not_idle_thread thread s'a; not_idle_thread (cur_thread s'a) s'a; st_tcb_at active thread s'a; valid_etcbs s'a; tcb_bound_notification x2 = Some x2a; get_tcb thread s'a = Some x2; kheap s'a thread = Some (TCB x2); valid_objs s'a; pspace_aligned s'a; pspace_distinct s'a; if_live_then_nonz_cap s'a; zombies_final s'a; sym_refs (state_refs_of s'a); sym_refs (state_hyp_refs_of s'a); valid_mdb s'a; valid_ioc s'a; valid_idle s'a; only_idle s'a; if_unsafe_then_cap s'a; valid_reply_caps s'a; valid_reply_masters s'a; valid_global_refs s'a; valid_arch_state s'a; valid_irq_node s'a; valid_irq_handlers s'a; valid_irq_states s'a; valid_machine_state s'a; valid_vspace_objs s'a; valid_arch_caps s'a; valid_global_objs s'a; valid_kernel_mappings s'a; equal_kernel_mappings s'a; valid_asid_map s'a; valid_global_vspace_mappings s'a; pspace_in_kernel_window s'a; cap_refs_in_kernel_window s'a; pspace_respects_device_region s'a; cap_refs_respects_device_region s'a; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s'a \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr thread (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s'a; case tcb_fault x2 of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler x2) = word_bits; valid_arch_tcb (tcb_arch x2) s'a; kheap s'a x2a = Some (kernel_object.Notification ntfn); is_ntfn (kernel_object.Notification ntfn); \<not> isActive ntfn\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (receive_sync thread epptr (AllowGrant \<in> ep_rights)) (case rv of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (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 epptr $ 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;
Ipc_A.do_ipc_transfer sender (Some epptr) (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> ep_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 thread (BlockedOnReceive epptr \<lparr>receiver_can_grant = AllowGrant \<in> ep_rights\<rparr>);
set_endpoint epptr (RecvEP (queue @ [thread]))
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 2. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 3. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal (3 subgoals):
 1. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ko. (=) s' and ko_at (kernel_object.Endpoint ko) epptr\<rbrace>
 2. \<And>ep_badge ep_rights s s' sa. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_endpoint epptr \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>ep_badge ep_rights s s'. \<lbrakk>ep_id = epptr; tcb_id_receiver = thread; ep_cap = cap.EndpointCap epptr ep_badge ep_rights; s = transform s'; True; (ep_at epptr and not_idle_thread thread and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active thread and valid_state and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_endpoint epptr) proof (prove)
goal:
No subgoals!