theory Syscall_AI

lemma send_fault_ipc_st_tcb_at_runnable:
  "\<lbrace>st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s)) and tcb_at t' and K (t' \<noteq> t)\<rbrace> send_fault_ipc t' f \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>" unfolding send_fault_ipc_def apply (rule hoare_pre, wp) apply (clarsimp simp: Let_def) apply wpc apply (wp send_ipc_st_tcb_at_runnable thread_set_no_change_tcb_state thread_set_refs_trivial
                          hoare_vcg_all_lift_R thread_get_wp
                        | clarsimp
                        | wp (once) hoare_drop_imps)+ apply (clarsimp simp:  pred_tcb_at_def obj_at_def is_tcb) 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 tcb_at t' and K (t' \<noteq> t)\<rbrace> send_fault_ipc t' f \<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 tcb_at t' and K (t' \<noteq> t)\<rbrace> doE handler_cptr <- liftE $ thread_get tcb_fault_handler t';
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap t' handler_cptr;
let fa = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some f)) t';
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True t' (cap_ep_ptr handler_cap)
od else throwError fa | _ \<Rightarrow> throwError fa
odE \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>handler_cptr handler_cap. \<lbrace>?B6 handler_cptr handler_cap\<rbrace> let fa = CapFault (of_bl handler_cptr) False (MissingCapability 0) in case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some f)) t';
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True t' (cap_ep_ptr handler_cap)
od else throwError fa | _ \<Rightarrow> throwError fa \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 2. \<And>handler_cptr. \<lbrace>?B5 handler_cptr\<rbrace> cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap t' handler_cptr \<lbrace>?B6 handler_cptr\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 3. \<lbrace>?Q\<rbrace> liftE $ thread_get tcb_fault_handler t' \<lbrace>?B5\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 4. \<And>s. (st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s)) and tcb_at t' and K (t' \<noteq> t)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>handler_cptr handler_cap. \<lbrace>?B6 handler_cptr handler_cap\<rbrace> case handler_cap of EndpointCap ref badge rights \<Rightarrow> if AllowSend \<in> rights \<and> (AllowGrant \<in> rights \<or> AllowGrantReply \<in> rights) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some f)) t';
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True t' (cap_ep_ptr handler_cap)
od else throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) | _ \<Rightarrow> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 2. \<And>handler_cptr. \<lbrace>?B5 handler_cptr\<rbrace> cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap t' handler_cptr \<lbrace>?B6 handler_cptr\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 3. \<lbrace>?Q\<rbrace> liftE $ thread_get tcb_fault_handler t' \<lbrace>?B5\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 4. \<And>s. (st_tcb_at runnable t and (\<lambda>s. sym_refs (state_refs_of s)) and tcb_at t' and K (t' \<noteq> t)) s \<Longrightarrow> ?Q s proof (prove)
goal (15 subgoals):
 1. \<And>handler_cptr handler_cap. handler_cap = NullCap \<Longrightarrow> \<lbrace>?R59 handler_cptr handler_cap\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 2. \<And>handler_cptr handler_cap x21 x22 x23 x24. handler_cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>?R60 handler_cptr handler_cap x21 x22 x23 x24\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 3. \<And>handler_cptr handler_cap x31 x32 x33. handler_cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>?R61 handler_cptr handler_cap x31 x32 x33\<rbrace> if AllowSend \<in> x33 \<and> (AllowGrant \<in> x33 \<or> AllowGrantReply \<in> x33) then liftE $ do thread_set (tcb_fault_update (\<lambda>_. Some f)) t';
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> x33) True t' (cap_ep_ptr handler_cap)
od else throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 4. \<And>handler_cptr handler_cap x41 x42 x43. handler_cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>?R62 handler_cptr handler_cap x41 x42 x43\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 5. \<And>handler_cptr handler_cap x51 x52 x53. handler_cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>?R63 handler_cptr handler_cap x51 x52 x53\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 6. \<And>handler_cptr handler_cap x61 x62 x63. handler_cap = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>?R64 handler_cptr handler_cap x61 x62 x63\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 7. \<And>handler_cptr handler_cap x7. handler_cap = ThreadCap x7 \<Longrightarrow> \<lbrace>?R65 handler_cptr handler_cap x7\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 8. \<And>handler_cptr handler_cap. handler_cap = DomainCap \<Longrightarrow> \<lbrace>?R66 handler_cptr handler_cap\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 9. \<And>handler_cptr handler_cap. handler_cap = IRQControlCap \<Longrightarrow> \<lbrace>?R67 handler_cptr handler_cap\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 10. \<And>handler_cptr handler_cap x10. handler_cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>?R68 handler_cptr handler_cap x10\<rbrace> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>, \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
A total of 15 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>st_tcb_at runnable t s; sym_refs (state_refs_of s); tcb_at t' s; t' \<noteq> t\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) t' s proof (prove)
goal:
No subgoals!