theory Syscall_AI

lemma send_ipc_st_tcb_at_runnable:
  "\<lbrace>st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s)) and K (t' \<noteq> t) \<rbrace>
   send_ipc block call badge can_grant can_grant_reply t' epptr
   \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>" unfolding send_ipc_def apply (rule hoare_gen_asm) apply (wpc | wp sts_st_tcb_at_other | clarsimp)+ apply (simp add: setup_caller_cap_def) apply (rule conjI) apply (wpc
                | wp sts_st_tcb_at_other dxo_wp_weak hoare_drop_imps
                | clarsimp simp: if_fun_split)+ apply (wp get_simple_ko_wp) apply clarsimp apply (drule st_tcb_at_state_refs_ofD) apply (drule (1) sym_refs_ko_atD) apply clarsimp apply (case_tac ts; clarsimp simp: obj_at_def state_refs_of_def dest!:refs_in_tcb_bound_refs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s)) and K (t' \<noteq> t)\<rbrace> send_ipc block call badge can_grant can_grant_reply t' epptr \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s)) and K (t' \<noteq> t)\<rbrace> do ep <- get_endpoint epptr;
case (ep, block) of (IdleEP, True) \<Rightarrow> do set_thread_state t' (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>);
set_endpoint epptr $ SendEP [t']
od | (IdleEP, False) \<Rightarrow> return () | (SendEP queue, True) \<Rightarrow> do set_thread_state t' (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>);
set_endpoint epptr $ SendEP (queue @ [t'])
od | (SendEP queue, False) \<Rightarrow> return () | (RecvEP [], x) \<Rightarrow> fail | (RecvEP (dest # queue), x) \<Rightarrow> do set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state dest;
reply_can_grant <- case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer t' (Some epptr) badge can_grant dest;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state dest Running;
do_extended_op (possible_switch_to dest);
when call $ if can_grant \<or> can_grant_reply then setup_caller_cap t' dest reply_can_grant else set_thread_state t' Inactive
od
od \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace> proof (prove)
goal (1 subgoal):
 1. t' \<noteq> t \<Longrightarrow> \<lbrace>st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s))\<rbrace> do ep <- get_endpoint epptr;
case (ep, block) of (IdleEP, True) \<Rightarrow> do set_thread_state t' (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>);
set_endpoint epptr $ SendEP [t']
od | (IdleEP, False) \<Rightarrow> return () | (SendEP queue, True) \<Rightarrow> do set_thread_state t' (BlockedOnSend epptr \<lparr>sender_badge = badge, sender_can_grant = can_grant, sender_can_grant_reply = can_grant_reply, sender_is_call = call\<rparr>);
set_endpoint epptr $ SendEP (queue @ [t'])
od | (SendEP queue, False) \<Rightarrow> return () | (RecvEP [], x) \<Rightarrow> fail | (RecvEP (dest # queue), x) \<Rightarrow> do set_endpoint epptr $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state dest;
reply_can_grant <- case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer t' (Some epptr) badge can_grant dest;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state dest Running;
do_extended_op (possible_switch_to dest);
when call $ if can_grant \<or> can_grant_reply then setup_caller_cap t' dest reply_can_grant else set_thread_state t' Inactive
od
od \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>x21 x22 recv_state reply_can_grant. \<lbrakk>t' \<noteq> t; call; can_grant \<or> can_grant_reply\<rbrakk> \<Longrightarrow> \<lbrace>?Q83 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state reply_can_grant () ()\<rbrace> setup_caller_cap t' x21 reply_can_grant \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 2. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa xb. \<lbrakk>t' \<noteq> t; ep = RecvEP x3; x3 = x21 # x22; call; \<not> (can_grant \<or> can_grant_reply)\<rbrakk> \<Longrightarrow> \<lbrace>?R83 ep x3 x21 x22 x recv_state reply_can_grant xa xb\<rbrace> set_thread_state t' Inactive \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 3. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa. \<lbrakk>t' \<noteq> t; ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B77 ep x3 x21 x22 x recv_state reply_can_grant xa\<rbrace> do_extended_op (possible_switch_to x21) \<lbrace>\<lambda>xb. if call then \<lambda>s. (can_grant \<or> can_grant_reply \<longrightarrow> ?Q83 ep x3 x21 x22 x recv_state reply_can_grant xa xb s) \<and> (\<not> (can_grant \<or> can_grant_reply) \<longrightarrow> ?R83 ep x3 x21 x22 x recv_state reply_can_grant xa xb s) else st_tcb_at runnable t\<rbrace>
 4. \<And>ep x3 x21 x22 x recv_state reply_can_grant. \<lbrakk>t' \<noteq> t; ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B76 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace> set_thread_state x21 Running \<lbrace>?B77 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace>
 5. \<And>ep x3 x21 x22 x recv_state. \<lbrakk>t' \<noteq> t; ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B75 ep x3 x21 x22 x recv_state\<rbrace> case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer t' (Some epptr) badge can_grant x21;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail \<lbrace>?B76 ep x3 x21 x22 x recv_state\<rbrace>
 6. \<And>ep x3 x21 x22 x. \<lbrakk>t' \<noteq> t; ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B73 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B75 ep x3 x21 x22 x\<rbrace>
 7. \<And>ep x3 x21 x22. \<lbrakk>t' \<noteq> t; ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R67 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B73 ep x3 x21 x22\<rbrace>
 8. t' \<noteq> t \<Longrightarrow> \<lbrace>?Q2\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (st_tcb_at runnable t and K (t \<noteq> t')) s) \<and> (block = False \<longrightarrow> st_tcb_at runnable t s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (st_tcb_at runnable t and K (t \<noteq> t')) s) \<and> (block = False \<longrightarrow> st_tcb_at runnable t s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R67 ep x xa xb s))\<rbrace>
 9. \<And>s. \<lbrakk>t' \<noteq> t; (st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s))) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (9 subgoals):
 1. \<And>x21 x22 recv_state reply_can_grant. \<lbrakk>t' \<noteq> t; call; can_grant \<or> can_grant_reply\<rbrakk> \<Longrightarrow> (reply_can_grant \<longrightarrow> \<lbrace>?Q83 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state True () ()\<rbrace> do y <- set_thread_state t' BlockedOnReply;
cap_insert (ReplyCap t' False {AllowGrant, AllowWrite}) (t', tcb_cnode_index 2) (x21, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>) \<and> (\<not> reply_can_grant \<longrightarrow> \<lbrace>?Q83 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state False () ()\<rbrace> do y <- set_thread_state t' BlockedOnReply;
cap_insert (ReplyCap t' False {AllowWrite}) (t', tcb_cnode_index 2) (x21, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>)
 2. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa xb. \<lbrakk>t' \<noteq> t; ep = RecvEP x3; x3 = x21 # x22; call; \<not> (can_grant \<or> can_grant_reply)\<rbrakk> \<Longrightarrow> \<lbrace>?R83 ep x3 x21 x22 x recv_state reply_can_grant xa xb\<rbrace> set_thread_state t' Inactive \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 3. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa. \<lbrakk>t' \<noteq> t; ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B77 ep x3 x21 x22 x recv_state reply_can_grant xa\<rbrace> do_extended_op (possible_switch_to x21) \<lbrace>\<lambda>xb. if call then \<lambda>s. (can_grant \<or> can_grant_reply \<longrightarrow> ?Q83 ep x3 x21 x22 x recv_state reply_can_grant xa xb s) \<and> (\<not> (can_grant \<or> can_grant_reply) \<longrightarrow> ?R83 ep x3 x21 x22 x recv_state reply_can_grant xa xb s) else st_tcb_at runnable t\<rbrace>
 4. \<And>ep x3 x21 x22 x recv_state reply_can_grant. \<lbrakk>t' \<noteq> t; ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B76 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace> set_thread_state x21 Running \<lbrace>?B77 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace>
 5. \<And>ep x3 x21 x22 x recv_state. \<lbrakk>t' \<noteq> t; ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B75 ep x3 x21 x22 x recv_state\<rbrace> case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer t' (Some epptr) badge can_grant x21;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail \<lbrace>?B76 ep x3 x21 x22 x recv_state\<rbrace>
 6. \<And>ep x3 x21 x22 x. \<lbrakk>t' \<noteq> t; ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B73 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B75 ep x3 x21 x22 x\<rbrace>
 7. \<And>ep x3 x21 x22. \<lbrakk>t' \<noteq> t; ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R67 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B73 ep x3 x21 x22\<rbrace>
 8. t' \<noteq> t \<Longrightarrow> \<lbrace>?Q2\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (st_tcb_at runnable t and K (t \<noteq> t')) s) \<and> (block = False \<longrightarrow> st_tcb_at runnable t s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (st_tcb_at runnable t and K (t \<noteq> t')) s) \<and> (block = False \<longrightarrow> st_tcb_at runnable t s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R67 ep x xa xb s))\<rbrace>
 9. \<And>s. \<lbrakk>t' \<noteq> t; (st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s))) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (10 subgoals):
 1. \<And>x21 x22 recv_state reply_can_grant. \<lbrakk>t' \<noteq> t; call; can_grant \<or> can_grant_reply\<rbrakk> \<Longrightarrow> reply_can_grant \<longrightarrow> \<lbrace>?Q83 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state True () ()\<rbrace> do y <- set_thread_state t' BlockedOnReply;
cap_insert (ReplyCap t' False {AllowGrant, AllowWrite}) (t', tcb_cnode_index 2) (x21, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 2. \<And>x21 x22 recv_state reply_can_grant. \<lbrakk>t' \<noteq> t; call; can_grant \<or> can_grant_reply\<rbrakk> \<Longrightarrow> \<not> reply_can_grant \<longrightarrow> \<lbrace>?Q83 (RecvEP (x21 # x22)) (x21 # x22) x21 x22 () recv_state False () ()\<rbrace> do y <- set_thread_state t' BlockedOnReply;
cap_insert (ReplyCap t' False {AllowWrite}) (t', tcb_cnode_index 2) (x21, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 3. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa xb. \<lbrakk>t' \<noteq> t; ep = RecvEP x3; x3 = x21 # x22; call; \<not> (can_grant \<or> can_grant_reply)\<rbrakk> \<Longrightarrow> \<lbrace>?R83 ep x3 x21 x22 x recv_state reply_can_grant xa xb\<rbrace> set_thread_state t' Inactive \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 4. \<And>ep x3 x21 x22 x recv_state reply_can_grant xa. \<lbrakk>t' \<noteq> t; ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B77 ep x3 x21 x22 x recv_state reply_can_grant xa\<rbrace> do_extended_op (possible_switch_to x21) \<lbrace>\<lambda>xb. if call then \<lambda>s. (can_grant \<or> can_grant_reply \<longrightarrow> ?Q83 ep x3 x21 x22 x recv_state reply_can_grant xa xb s) \<and> (\<not> (can_grant \<or> can_grant_reply) \<longrightarrow> ?R83 ep x3 x21 x22 x recv_state reply_can_grant xa xb s) else st_tcb_at runnable t\<rbrace>
 5. \<And>ep x3 x21 x22 x recv_state reply_can_grant. \<lbrakk>t' \<noteq> t; ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B76 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace> set_thread_state x21 Running \<lbrace>?B77 ep x3 x21 x22 x recv_state reply_can_grant\<rbrace>
 6. \<And>ep x3 x21 x22 x recv_state. \<lbrakk>t' \<noteq> t; ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B75 ep x3 x21 x22 x recv_state\<rbrace> case recv_state of BlockedOnReceive x data \<Rightarrow> do do_ipc_transfer t' (Some epptr) badge can_grant x21;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail \<lbrace>?B76 ep x3 x21 x22 x recv_state\<rbrace>
 7. \<And>ep x3 x21 x22 x. \<lbrakk>t' \<noteq> t; ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?B73 ep x3 x21 x22 x\<rbrace> get_thread_state x21 \<lbrace>?B75 ep x3 x21 x22 x\<rbrace>
 8. \<And>ep x3 x21 x22. \<lbrakk>t' \<noteq> t; ep = RecvEP x3; x3 = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R67 ep x3 x21 x22\<rbrace> set_endpoint epptr $ case x22 of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP x22 \<lbrace>?B73 ep x3 x21 x22\<rbrace>
 9. t' \<noteq> t \<Longrightarrow> \<lbrace>?Q2\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> (block = True \<longrightarrow> (st_tcb_at runnable t and K (t \<noteq> t')) s) \<and> (block = False \<longrightarrow> st_tcb_at runnable t s)) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> (block = True \<longrightarrow> (st_tcb_at runnable t and K (t \<noteq> t')) s) \<and> (block = False \<longrightarrow> st_tcb_at runnable t s)) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> (x = [] \<longrightarrow> True) \<and> (\<forall>xa xb. x = xa # xb \<longrightarrow> ?R67 ep x xa xb s))\<rbrace>
 10. \<And>s. \<lbrakk>t' \<noteq> t; (st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s))) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. t' \<noteq> t \<Longrightarrow> \<lbrace>?P'281\<rbrace> get_endpoint epptr \<lbrace>\<lambda>rv s. \<forall>x. rv = RecvEP x \<longrightarrow> (\<forall>xa. (\<exists>xb. x = xa # xb) \<longrightarrow> st_tcb_at runnable t s \<and> t \<noteq> xa \<and> st_tcb_at runnable t s \<and> t \<noteq> xa \<and> st_tcb_at runnable t s \<and> t \<noteq> xa \<and> st_tcb_at runnable t s \<and> t \<noteq> xa)\<rbrace>
 2. \<And>s. \<lbrakk>t' \<noteq> t; (st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s))) s\<rbrakk> \<Longrightarrow> ((st_tcb_at runnable t and K (t \<noteq> t')) s \<and> st_tcb_at runnable t s) \<and> st_tcb_at runnable t s \<and> ?P'281 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>t' \<noteq> t; (st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s))) s\<rbrakk> \<Longrightarrow> ((st_tcb_at runnable t and K (t \<noteq> t')) s \<and> st_tcb_at runnable t s) \<and> st_tcb_at runnable t s \<and> (\<forall>ntfn. ko_at (Endpoint ntfn) epptr s \<longrightarrow> (\<forall>x. ntfn = RecvEP x \<longrightarrow> (\<forall>xa. (\<exists>xb. x = xa # xb) \<longrightarrow> st_tcb_at runnable t s \<and> t \<noteq> xa \<and> st_tcb_at runnable t s \<and> t \<noteq> xa \<and> st_tcb_at runnable t s \<and> t \<noteq> xa \<and> st_tcb_at runnable t s \<and> t \<noteq> xa))) proof (prove)
goal (1 subgoal):
 1. \<And>s xb. \<lbrakk>t' \<noteq> t; st_tcb_at runnable t s; sym_refs (state_refs_of s); ko_at (Endpoint (RecvEP (t # xb))) epptr s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s xb. \<lbrakk>t' \<noteq> t; sym_refs (state_refs_of s); ko_at (Endpoint (RecvEP (t # xb))) epptr s; \<exists>ts ntfnptr. runnable ts \<and> obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s xb. \<lbrakk>t' \<noteq> t; sym_refs (state_refs_of s); \<exists>ts ntfnptr. runnable ts \<and> obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr; state_refs_of s epptr = refs_of (Endpoint (RecvEP (t # xb))) \<and> (\<forall>(x, tp)\<in>refs_of (Endpoint (RecvEP (t # xb))). obj_at (\<lambda>ko. (epptr, symreftype tp) \<in> refs_of ko) x s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s xb ts ntfnptr. \<lbrakk>t' \<noteq> t; sym_refs (state_refs_of s); state_refs_of s epptr = insert (t, EPRecv) (set xb \<times> {EPRecv}); runnable ts; obj_at (\<lambda>ko. (epptr, TCBBlockedRecv) \<in> refs_of ko) t s; \<forall>x\<in>set xb. obj_at (\<lambda>ko. (epptr, TCBBlockedRecv) \<in> refs_of ko) x s; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!