theory Syscall_AI

lemma handle_recv_st_tcb_at:
  "\<lbrace>invs and st_tcb_at runnable t and (\<lambda>s. cur_thread s \<noteq> t)\<rbrace> handle_recv True
  \<lbrace>\<lambda>rv s::det_ext state. st_tcb_at runnable t s\<rbrace>" apply (simp add: handle_recv_def Let_def ep_ntfn_cap_case_helper
             cong: if_cong) apply (rule hoare_pre) apply (wp handle_fault_st_tcb_at_runnable receive_ipc_st_tcb_at_runnable
             delete_caller_cap_sym_refs rai_pred_tcb_neq
             get_simple_ko_wp hoare_drop_imps hoare_vcg_all_lift_R) apply clarsimp apply wp+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and st_tcb_at runnable t and (\<lambda>s. cur_thread s \<noteq> t)\<rbrace> handle_recv True \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and st_tcb_at runnable t and (\<lambda>s. cur_thread s \<noteq> t)\<rbrace> do thread <- gets cur_thread;
ep_cptr <- liftM to_bl (as_user thread (getRegister cap_register));
cap_fault_on_failure (of_bl ep_cptr) True (doE ep_cap <- lookup_cap thread ep_cptr;
if is_ep_cap ep_cap then if AllowRecv \<in> cap_rights ep_cap then liftE (do y <- delete_caller_cap thread;
receive_ipc thread ep_cap True
od) else throwError (MissingCapability 0) else if is_ntfn_cap ep_cap then if AllowRecv \<in> cap_rights ep_cap then doE ntfn <- liftE (get_notification (cap_ep_ptr ep_cap));
if ntfn_bound_tcb ntfn = Some thread \<or> ntfn_bound_tcb ntfn = None then liftE (receive_signal thread ep_cap True) else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) else throwError (MissingCapability 0)
odE) <catch> handle_fault thread
od \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q12\<rbrace> do thread <- gets cur_thread;
ep_cptr <- liftM to_bl (as_user thread (getRegister cap_register));
cap_fault_on_failure (of_bl ep_cptr) True (doE ep_cap <- lookup_cap thread ep_cptr;
if is_ep_cap ep_cap then if AllowRecv \<in> cap_rights ep_cap then liftE (do y <- delete_caller_cap thread;
receive_ipc thread ep_cap True
od) else throwError (MissingCapability 0) else if is_ntfn_cap ep_cap then if AllowRecv \<in> cap_rights ep_cap then doE ntfn <- liftE (get_notification (cap_ep_ptr ep_cap));
if ntfn_bound_tcb ntfn = Some thread \<or> ntfn_bound_tcb ntfn = None then liftE (receive_signal thread ep_cap True) else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) else throwError (MissingCapability 0)
odE) <catch> handle_fault thread
od \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 2. \<And>s. (invs and st_tcb_at runnable t and (\<lambda>s. cur_thread s \<noteq> t)) s \<Longrightarrow> ?Q12 s proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>?B16 thread\<rbrace> as_user thread (getRegister cap_register) \<lbrace>(\<lambda>ep_cptr s. st_tcb_at runnable t s \<and> invs s \<and> K (thread \<noteq> t) s \<and> ((st_tcb_at runnable t s \<and> invs s \<and> K (thread \<noteq> t) s) \<and> st_tcb_at runnable t s \<and> invs s \<and> K (thread \<noteq> t) s \<and> True) \<and> ((\<forall>x. (st_tcb_at runnable t and K (thread \<noteq> t)) s \<and> st_tcb_at runnable t s \<and> invs s \<and> K (thread \<noteq> t) s \<and> True) \<and> st_tcb_at runnable t s \<and> invs s \<and> K (thread \<noteq> t) s \<and> True) \<and> st_tcb_at runnable t s \<and> invs s \<and> K (thread \<noteq> t) s \<and> True) \<circ> to_bl\<rbrace>
 2. \<lbrace>?Q12\<rbrace> gets cur_thread \<lbrace>?B16\<rbrace>
 3. \<And>s. (invs and st_tcb_at runnable t and (\<lambda>s. cur_thread s \<noteq> t)) s \<Longrightarrow> ?Q12 s proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>?B16 thread\<rbrace> as_user thread (getRegister cap_register) \<lbrace>\<lambda>ep_cptr s. st_tcb_at runnable t s \<and> invs s \<and> thread \<noteq> t \<and> st_tcb_at runnable t s \<and> invs s \<and> thread \<noteq> t \<and> st_tcb_at runnable t s \<and> thread \<noteq> t \<and> st_tcb_at runnable t s \<and> invs s \<and> thread \<noteq> t\<rbrace>
 2. \<lbrace>?Q12\<rbrace> gets cur_thread \<lbrace>?B16\<rbrace>
 3. \<And>s. (invs and st_tcb_at runnable t and (\<lambda>s. cur_thread s \<noteq> t)) s \<Longrightarrow> ?Q12 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and st_tcb_at runnable t and (\<lambda>s. cur_thread s \<noteq> t)) s \<Longrightarrow> st_tcb_at runnable t s \<and> invs s \<and> cur_thread s \<noteq> t \<and> st_tcb_at runnable t s \<and> invs s \<and> cur_thread s \<noteq> t \<and> st_tcb_at runnable t s \<and> cur_thread s \<noteq> t \<and> st_tcb_at runnable t s \<and> invs s \<and> cur_thread s \<noteq> t proof (prove)
goal:
No subgoals!