theory Ipc_AI

lemma ri_makes_simple:
  "\<lbrace>st_tcb_at simple t' and K (t \<noteq> t') :: 'state_ext state \<Rightarrow> bool\<rbrace>
     receive_ipc t cap is_blocking
   \<lbrace>\<lambda>rv. st_tcb_at simple t'\<rbrace>" (is "\<lbrace>?pre\<rbrace> _ \<lbrace>_\<rbrace>") apply (rule hoare_gen_asm) apply (simp add: receive_ipc_def split_def) apply (case_tac cap, simp_all) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (rule hoare_seq_ext [OF _ gbn_sp]) apply (rule hoare_seq_ext) apply (rename_tac ep I DO x CARE NOT) apply (rule_tac R="ko_at (Endpoint x) ep and ?pre" in hoare_vcg_if_split) apply (wp complete_signal_invs) apply (case_tac x, simp_all) apply (rule hoare_pre, wpc) apply (wp sts_st_tcb_at_cases, simp) apply (simp add: do_nbrecv_failed_transfer_def, wp) apply clarsimp apply (rule hoare_seq_ext [OF _ assert_sp]) apply (rule hoare_seq_ext [where B="\<lambda>s. st_tcb_at simple t'"]) apply (rule hoare_seq_ext [OF _ gts_sp]) apply (rule hoare_pre) apply (wp setup_caller_cap_makes_simple sts_st_tcb_at_cases
                hoare_vcg_all_lift hoare_vcg_const_imp_lift
                hoare_drop_imps
           | wpc | simp)+ apply (fastforce simp: pred_tcb_at_def obj_at_def) apply (wp, simp) apply (wp sts_st_tcb_at_cases | rule hoare_pre, wpc | simp add: do_nbrecv_failed_transfer_def)+ apply (wp get_simple_ko_wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' and K (t \<noteq> t')\<rbrace> receive_ipc t cap is_blocking \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> receive_ipc t cap is_blocking \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> do p <- case cap of EndpointCap ref badge rights \<Rightarrow> return (ref, rights) | _ \<Rightarrow> fail;
ep <- get_endpoint (fst p);
ntfnptr <- get_bound_notification t;
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) t else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst p) \<lparr>receiver_can_grant = AllowGrant \<in> snd p\<rparr>);
set_endpoint (fst p) (RecvEP [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint (fst p) $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some (fst p)) (sender_badge data) (sender_can_grant data) t;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender t (AllowGrant \<in> snd p) 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 t (BlockedOnReceive (fst p) \<lparr>receiver_can_grant = AllowGrant \<in> snd p\<rparr>);
set_endpoint (fst p) (RecvEP (queue @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> do ep <- get_endpoint x31;
ntfnptr <- get_bound_notification t;
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) t else case ep of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (x31, x33)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (x31, x33)\<rparr>);
set_endpoint (fst (x31, x33)) (RecvEP [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint (fst (x31, x33)) $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some (fst (x31, x33))) (sender_badge data) (sender_can_grant data) t;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender t (AllowGrant \<in> snd (x31, 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 t (BlockedOnReceive (fst (x31, x33)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (x31, x33)\<rparr>);
set_endpoint (fst (x31, x33)) (RecvEP (queue @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 x. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> do ntfnptr <- get_bound_notification t;
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) t else case x of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (x31, x33)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (x31, x33)\<rparr>);
set_endpoint (fst (x31, x33)) (RecvEP [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint (fst (x31, x33)) $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some (fst (x31, x33))) (sender_badge data) (sender_can_grant data) t;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender t (AllowGrant \<in> snd (x31, 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 t (BlockedOnReceive (fst (x31, x33)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (x31, x33)\<rparr>);
set_endpoint (fst (x31, x33)) (RecvEP (queue @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 x ntfnptr. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t and (ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t')\<rbrace> do ntfn <- case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x;
if (\<exists>y. ntfnptr = Some y) \<and> isActive ntfn then complete_signal (the ntfnptr) t else case x of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (x31, x33)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (x31, x33)\<rparr>);
set_endpoint (fst (x31, x33)) (RecvEP [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint (fst (x31, x33)) $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some (fst (x31, x33))) (sender_badge data) (sender_can_grant data) t;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender t (AllowGrant \<in> snd (x31, 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 t (BlockedOnReceive (fst (x31, x33)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (x31, x33)\<rparr>);
set_endpoint (fst (x31, x33)) (RecvEP (queue @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 x ntfnptr ntfn. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>?B11 x31 x32 x33 x ntfnptr ntfn\<rbrace> if (\<exists>y. ntfnptr = Some y) \<and> isActive ntfn then complete_signal (the ntfnptr) t else case x of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (x31, x33)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (x31, x33)\<rparr>);
set_endpoint (fst (x31, x33)) (RecvEP [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint (fst (x31, x33)) $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some (fst (x31, x33))) (sender_badge data) (sender_can_grant data) t;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender t (AllowGrant \<in> snd (x31, 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 t (BlockedOnReceive (fst (x31, x33)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (x31, x33)\<rparr>);
set_endpoint (fst (x31, x33)) (RecvEP (queue @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 2. \<And>x31 x32 x33 x ntfnptr. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t and (ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t')\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>?B11 x31 x32 x33 x ntfnptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ep I DO x CARE NOT. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO\<rbrakk> \<Longrightarrow> \<lbrace>?B11 ep I DO x CARE NOT\<rbrace> if (\<exists>y. CARE = Some y) \<and> isActive NOT then complete_signal (the CARE) t else case x of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint (fst (ep, DO)) $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some (fst (ep, DO))) (sender_badge data) (sender_can_grant data) t;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender t (AllowGrant \<in> snd (ep, DO)) 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 t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP (queue @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 2. \<And>x31 x32 x33 x ntfnptr. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t and (ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t')\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>?B11 x31 x32 x33 x ntfnptr\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ep I DO x CARE NOT. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; (\<exists>y. CARE = Some y) \<and> isActive NOT\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 ep I DO x CARE NOT\<rbrace> complete_signal (the CARE) t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 2. \<And>ep I DO x CARE NOT. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; \<not> ((\<exists>y. CARE = Some y) \<and> isActive NOT)\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint x) ep and (st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' and K (t \<noteq> t'))\<rbrace> case x of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint (fst (ep, DO)) $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some (fst (ep, DO))) (sender_badge data) (sender_can_grant data) t;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender t (AllowGrant \<in> snd (ep, DO)) 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 t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP (queue @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 3. \<And>x31 x32 x33 x ntfnptr. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t and (ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t')\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>NOT s. ((\<exists>y. ntfnptr = Some y) \<and> isActive NOT \<longrightarrow> ?Q14 x31 x32 x33 x ntfnptr NOT s) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive NOT) \<longrightarrow> (ko_at (Endpoint x) x31 and (st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' and K (t \<noteq> t'))) s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ep I DO x CARE NOT. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; \<not> ((\<exists>y. CARE = Some y) \<and> isActive NOT)\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint x) ep and (st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' and K (t \<noteq> t'))\<rbrace> case x of IdleEP \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | SendEP q \<Rightarrow> do assert (q \<noteq> []);
queue <- return $ tl q;
sender <- return $ hd q;
set_endpoint (fst (ep, DO)) $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue;
sender_state <- get_thread_state sender;
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
do_ipc_transfer sender (Some (fst (ep, DO))) (sender_badge data) (sender_can_grant data) t;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap sender t (AllowGrant \<in> snd (ep, DO)) 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 t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP (queue @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 2. \<And>x31 x32 x33 x ntfnptr. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t and (ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t')\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>NOT s. ((\<exists>y. ntfnptr = Some y) \<and> isActive NOT \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (\<not> ((\<exists>y. ntfnptr = Some y) \<and> isActive NOT) \<longrightarrow> (ko_at (Endpoint x) x31 and (st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' and K (t \<noteq> t'))) s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ep I DO x CARE NOT. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = IdleEP\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint IdleEP) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 2. \<And>ep I DO x CARE NOT x2. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (SendEP x2)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> do y <- assert (x2 \<noteq> []);
y <- set_endpoint ep (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2));
sender_state <- get_thread_state (hd x2);
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd x2) (Some ep) (sender_badge data) (sender_can_grant data) t;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap (hd x2) t (AllowGrant \<in> DO) else set_thread_state (hd x2) Inactive else do y <- set_thread_state (hd x2) Running;
do_extended_op (possible_switch_to (hd x2))
od
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 3. \<And>ep I DO x CARE NOT x3. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP (x3 @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 4. \<And>x31 x32 x33 x ntfnptr. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t and (ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t')\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>NOT s. ((\<exists>y. ntfnptr = Some y) \<and> isActive NOT \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (ntfnptr = None \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (\<not> isActive NOT \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ep I DO x CARE NOT. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = IdleEP; is_blocking = True\<rbrakk> \<Longrightarrow> \<lbrace>?R27 ep I DO x CARE NOT\<rbrace> do set_thread_state t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP [t])
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 2. \<And>ep I DO x CARE NOT. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = IdleEP; is_blocking = False\<rbrakk> \<Longrightarrow> \<lbrace>?R26 ep I DO x CARE NOT\<rbrace> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 3. \<And>ep I DO x CARE NOT s. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = IdleEP; (ko_at (Endpoint IdleEP) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t') s\<rbrakk> \<Longrightarrow> (is_blocking = True \<longrightarrow> ?R27 ep I DO x CARE NOT s) \<and> (is_blocking = False \<longrightarrow> ?R26 ep I DO x CARE NOT s)
 4. \<And>ep I DO x CARE NOT x2. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (SendEP x2)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> do y <- assert (x2 \<noteq> []);
y <- set_endpoint ep (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2));
sender_state <- get_thread_state (hd x2);
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd x2) (Some ep) (sender_badge data) (sender_can_grant data) t;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap (hd x2) t (AllowGrant \<in> DO) else set_thread_state (hd x2) Inactive else do y <- set_thread_state (hd x2) Running;
do_extended_op (possible_switch_to (hd x2))
od
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 5. \<And>ep I DO x CARE NOT x3. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP (x3 @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 6. \<And>x31 x32 x33 x ntfnptr. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t and (ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t')\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>NOT s. ((\<exists>y. ntfnptr = Some y) \<and> isActive NOT \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (ntfnptr = None \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (\<not> isActive NOT \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ep I DO x CARE NOT. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = IdleEP; \<not> is_blocking\<rbrakk> \<Longrightarrow> \<lbrace>?R26 ep I DO IdleEP CARE NOT\<rbrace> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 2. \<And>ep I DO x CARE NOT s. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = IdleEP; (ko_at (Endpoint IdleEP) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t') s\<rbrakk> \<Longrightarrow> (is_blocking = True \<longrightarrow> (t = t' \<longrightarrow> inactive (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>) \<or> BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr> = Running \<or> BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr> = Restart \<or> idle (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>) \<or> awaiting_reply (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>)) \<and> (t \<noteq> t' \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s)) \<and> (is_blocking = False \<longrightarrow> ?R26 ep I DO x CARE NOT s)
 3. \<And>ep I DO x CARE NOT x2. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (SendEP x2)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> do y <- assert (x2 \<noteq> []);
y <- set_endpoint ep (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2));
sender_state <- get_thread_state (hd x2);
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd x2) (Some ep) (sender_badge data) (sender_can_grant data) t;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap (hd x2) t (AllowGrant \<in> DO) else set_thread_state (hd x2) Inactive else do y <- set_thread_state (hd x2) Running;
do_extended_op (possible_switch_to (hd x2))
od
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 4. \<And>ep I DO x CARE NOT x3. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP (x3 @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 5. \<And>x31 x32 x33 x ntfnptr. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t and (ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t')\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>NOT s. ((\<exists>y. ntfnptr = Some y) \<and> isActive NOT \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (ntfnptr = None \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (\<not> isActive NOT \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ep I DO x CARE NOT s. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = IdleEP; (ko_at (Endpoint IdleEP) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t') s\<rbrakk> \<Longrightarrow> (is_blocking = True \<longrightarrow> (t = t' \<longrightarrow> inactive (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>) \<or> BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr> = Running \<or> BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr> = Restart \<or> idle (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>) \<or> awaiting_reply (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>)) \<and> (t \<noteq> t' \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s)) \<and> (is_blocking = False \<longrightarrow> st_tcb_at (\<lambda>a. inactive a \<or> a = Running \<or> a = Restart \<or> idle a \<or> awaiting_reply a) t' s)
 2. \<And>ep I DO x CARE NOT x2. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (SendEP x2)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> do y <- assert (x2 \<noteq> []);
y <- set_endpoint ep (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2));
sender_state <- get_thread_state (hd x2);
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd x2) (Some ep) (sender_badge data) (sender_can_grant data) t;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap (hd x2) t (AllowGrant \<in> DO) else set_thread_state (hd x2) Inactive else do y <- set_thread_state (hd x2) Running;
do_extended_op (possible_switch_to (hd x2))
od
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 3. \<And>ep I DO x CARE NOT x3. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP (x3 @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 4. \<And>x31 x32 x33 x ntfnptr. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t and (ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t')\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>NOT s. ((\<exists>y. ntfnptr = Some y) \<and> isActive NOT \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (ntfnptr = None \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (\<not> isActive NOT \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ep I DO x CARE NOT x2. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (SendEP x2)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> do y <- assert (x2 \<noteq> []);
y <- set_endpoint ep (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2));
sender_state <- get_thread_state (hd x2);
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd x2) (Some ep) (sender_badge data) (sender_can_grant data) t;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap (hd x2) t (AllowGrant \<in> DO) else set_thread_state (hd x2) Inactive else do y <- set_thread_state (hd x2) Running;
do_extended_op (possible_switch_to (hd x2))
od
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 2. \<And>ep I DO x CARE NOT x3. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP (x3 @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 3. \<And>x31 x32 x33 x ntfnptr. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t and (ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t')\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>NOT s. ((\<exists>y. ntfnptr = Some y) \<and> isActive NOT \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (ntfnptr = None \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (\<not> isActive NOT \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ep I DO x CARE NOT x2 y. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (ko_at (Endpoint (SendEP x2)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t') s \<and> x2 \<noteq> []\<rbrace> do y <- set_endpoint ep (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2));
sender_state <- get_thread_state (hd x2);
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd x2) (Some ep) (sender_badge data) (sender_can_grant data) t;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap (hd x2) t (AllowGrant \<in> DO) else set_thread_state (hd x2) Inactive else do y <- set_thread_state (hd x2) Running;
do_extended_op (possible_switch_to (hd x2))
od
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 2. \<And>ep I DO x CARE NOT x3. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP (x3 @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 3. \<And>x31 x32 x33 x ntfnptr. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t and (ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t')\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>NOT s. ((\<exists>y. ntfnptr = Some y) \<and> isActive NOT \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (ntfnptr = None \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (\<not> isActive NOT \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ep I DO x CARE NOT x2 y ya. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> do sender_state <- get_thread_state (hd x2);
data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd x2) (Some ep) (sender_badge data) (sender_can_grant data) t;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap (hd x2) t (AllowGrant \<in> DO) else set_thread_state (hd x2) Inactive else do y <- set_thread_state (hd x2) Running;
do_extended_op (possible_switch_to (hd x2))
od
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 2. \<And>ep I DO x CARE NOT x2 y. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (ko_at (Endpoint (SendEP x2)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t') s \<and> x2 \<noteq> []\<rbrace> set_endpoint ep (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) \<lbrace>\<lambda>s. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 3. \<And>ep I DO x CARE NOT x3. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP (x3 @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 4. \<And>x31 x32 x33 x ntfnptr. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t and (ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t')\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>NOT s. ((\<exists>y. ntfnptr = Some y) \<and> isActive NOT \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (ntfnptr = None \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (\<not> isActive NOT \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ep I DO x CARE NOT x2 y ya sender_state. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>st_tcb_at ((=) sender_state) (hd x2) and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> do data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd x2) (Some ep) (sender_badge data) (sender_can_grant data) t;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap (hd x2) t (AllowGrant \<in> DO) else set_thread_state (hd x2) Inactive else do y <- set_thread_state (hd x2) Running;
do_extended_op (possible_switch_to (hd x2))
od
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 2. \<And>ep I DO x CARE NOT x2 y. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (ko_at (Endpoint (SendEP x2)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t') s \<and> x2 \<noteq> []\<rbrace> set_endpoint ep (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) \<lbrace>\<lambda>s. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 3. \<And>ep I DO x CARE NOT x3. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP (x3 @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 4. \<And>x31 x32 x33 x ntfnptr. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t and (ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t')\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>NOT s. ((\<exists>y. ntfnptr = Some y) \<and> isActive NOT \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (ntfnptr = None \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (\<not> isActive NOT \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ep I DO x CARE NOT x2 y ya sender_state. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q52 ep I DO x CARE NOT x2 y ya sender_state\<rbrace> do data <- case sender_state of BlockedOnSend ref x \<Rightarrow> return x | _ \<Rightarrow> fail;
y <- do_ipc_transfer (hd x2) (Some ep) (sender_badge data) (sender_can_grant data) t;
if sender_is_call data then if sender_can_grant data \<or> sender_can_grant_reply data then setup_caller_cap (hd x2) t (AllowGrant \<in> DO) else set_thread_state (hd x2) Inactive else do y <- set_thread_state (hd x2) Running;
do_extended_op (possible_switch_to (hd x2))
od
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 2. \<And>ep I DO x CARE NOT x2 y ya sender_state s. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = SendEP x2; (st_tcb_at ((=) sender_state) (hd x2) and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t') s\<rbrakk> \<Longrightarrow> ?Q52 ep I DO x CARE NOT x2 y ya sender_state s
 3. \<And>ep I DO x CARE NOT x2 y. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (ko_at (Endpoint (SendEP x2)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t') s \<and> x2 \<noteq> []\<rbrace> set_endpoint ep (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) \<lbrace>\<lambda>s. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 4. \<And>ep I DO x CARE NOT x3. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP (x3 @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 5. \<And>x31 x32 x33 x ntfnptr. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t and (ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t')\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>NOT s. ((\<exists>y. ntfnptr = Some y) \<and> isActive NOT \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (ntfnptr = None \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (\<not> isActive NOT \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ep I DO x CARE NOT x2 sender_state s. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = SendEP x2; st_tcb_at ((=) sender_state) (hd x2) s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s\<rbrakk> \<Longrightarrow> (\<exists>x xa. sender_state = BlockedOnSend x xa) \<longrightarrow> t' \<noteq> hd x2
 2. \<And>ep I DO x CARE NOT x2 y. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (ko_at (Endpoint (SendEP x2)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t') s \<and> x2 \<noteq> []\<rbrace> set_endpoint ep (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) \<lbrace>\<lambda>s. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 3. \<And>ep I DO x CARE NOT x3. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP (x3 @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 4. \<And>x31 x32 x33 x ntfnptr. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t and (ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t')\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>NOT s. ((\<exists>y. ntfnptr = Some y) \<and> isActive NOT \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (ntfnptr = None \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (\<not> isActive NOT \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ep I DO x CARE NOT x2 y. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (ko_at (Endpoint (SendEP x2)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t') s \<and> x2 \<noteq> []\<rbrace> set_endpoint ep (case tl x2 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (tl x2)) \<lbrace>\<lambda>s. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 2. \<And>ep I DO x CARE NOT x3. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP (x3 @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 3. \<And>x31 x32 x33 x ntfnptr. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t and (ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t')\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>NOT s. ((\<exists>y. ntfnptr = Some y) \<and> isActive NOT \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (ntfnptr = None \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (\<not> isActive NOT \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ep I DO x CARE NOT x3. \<lbrakk>t \<noteq> t'; cap = EndpointCap ep I DO; CARE = None \<or> \<not> isActive NOT; x = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) ep and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnReceive (fst (ep, DO)) \<lparr>receiver_can_grant = AllowGrant \<in> snd (ep, DO)\<rparr>);
set_endpoint (fst (ep, DO)) (RecvEP (x3 @ [t]))
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
 2. \<And>x31 x32 x33 x ntfnptr. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptr) t and (ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t')\<rbrace> case ntfnptr of None \<Rightarrow> return default_notification | Some x \<Rightarrow> get_notification x \<lbrace>\<lambda>NOT s. ((\<exists>y. ntfnptr = Some y) \<and> isActive NOT \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (ntfnptr = None \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (\<not> isActive NOT \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 x ntfnptr x2. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33; ntfnptr = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R355 x31 x32 x33 x (Some x2) x2\<rbrace> get_notification x2 \<lbrace>\<lambda>NOT s. (isActive NOT \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (\<not> isActive NOT \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s)\<rbrace>
 2. \<And>x31 x32 x33 x ntfnptr s. \<lbrakk>t \<noteq> t'; cap = EndpointCap x31 x32 x33; (bound_tcb_at ((=) ntfnptr) t and (ko_at (Endpoint x) x31 and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t')) s\<rbrakk> \<Longrightarrow> (ntfnptr = None \<longrightarrow> ((\<exists>y. ntfnptr = Some y) \<and> isActive default_notification \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (ntfnptr = None \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s) \<and> (\<not> isActive default_notification \<longrightarrow> ko_at (Endpoint x) x31 s \<and> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' s)) \<and> (\<forall>xa. ntfnptr = Some xa \<longrightarrow> ?R355 x31 x32 x33 x ntfnptr xa s) proof (prove)
goal:
No subgoals!