theory Ipc_AI

lemma hf_invs':
  assumes set_endpoint_Q[wp]: "\<And>a b.\<lbrace>Q\<rbrace> set_endpoint a b \<lbrace>\<lambda>_.Q\<rbrace>"
  assumes sts_Q[wp]: "\<And>a b. \<lbrace>Q\<rbrace> set_thread_state a b \<lbrace>\<lambda>_.Q\<rbrace>"
  assumes ext_Q[wp]: "\<And>a b. \<lbrace>Q and valid_objs\<rbrace> do_extended_op (possible_switch_to a) \<lbrace>\<lambda>_.Q\<rbrace>"
  assumes setup_caller_cap_Q[wp]: "\<And>send receive grant. \<lbrace>Q and valid_mdb\<rbrace> setup_caller_cap send receive grant \<lbrace>\<lambda>_.Q\<rbrace>"
  assumes do_ipc_transfer_Q[wp]: "\<And>a b c d e. \<lbrace>Q and valid_objs and valid_mdb\<rbrace> do_ipc_transfer a b c d e \<lbrace>\<lambda>_.Q\<rbrace>"
  assumes thread_set_Q[wp]: "\<And>a b. \<lbrace>Q\<rbrace> thread_set a b \<lbrace>\<lambda>_.Q\<rbrace>"
  notes si_invs''[wp] = si_invs'[where Q=Q]
  shows
  "\<lbrace>invs and Q and st_tcb_at active t and ex_nonz_cap_to t and (\<lambda>_. valid_fault f)\<rbrace>
   handle_fault t f
   \<lbrace>\<lambda>r (s::'state_ext state). invs s \<and> Q s\<rbrace>" apply (cases "valid_fault f"; clarsimp) apply (simp add: handle_fault_def) apply wp apply (simp add: handle_double_fault_def) apply (wp sts_invs_minor) apply (simp add: send_fault_ipc_def Let_def) apply (wpsimp wp: thread_set_invs_trivial
                     thread_set_no_change_tcb_state ex_nonz_cap_to_pres
                     thread_set_cte_wp_at_trivial
                     hoare_vcg_all_lift_R
          | clarsimp simp: tcb_cap_cases_def
          | erule disjE)+ apply (wpe lookup_cap_ex_cap) apply (wpsimp wp: hoare_vcg_all_lift_R
        | strengthen reply_cap_doesnt_exist_strg
        | wp (once) hoare_drop_imps)+ apply (simp add: conj_comms) apply (fastforce elim!: pred_tcb_weakenE
               simp: invs_def valid_state_def valid_idle_def st_tcb_def2
                     idle_no_ex_cap pred_tcb_def2
              split: Structures_A.thread_state.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and Q and st_tcb_at active t and ex_nonz_cap_to t and (\<lambda>_. valid_fault f)\<rbrace> handle_fault t f \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. valid_fault f \<Longrightarrow> \<lbrace>invs and Q and st_tcb_at active t and ex_nonz_cap_to t\<rbrace> handle_fault t f \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. valid_fault f \<Longrightarrow> \<lbrace>invs and Q and st_tcb_at active t and ex_nonz_cap_to t\<rbrace> do _ <- gets_the (get_tcb t);
send_fault_ipc t f <catch> handle_double_fault t f
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>uu_ x. valid_fault f \<Longrightarrow> \<lbrace>?E9 uu_ x\<rbrace> handle_double_fault t f x \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 2. \<And>uu_. valid_fault f \<Longrightarrow> \<lbrace>?B8 uu_\<rbrace> send_fault_ipc t f \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>, \<lbrace>?E9 uu_\<rbrace>
 3. valid_fault f \<Longrightarrow> \<lbrace>?Q7\<rbrace> gets_the (get_tcb t) \<lbrace>?B8\<rbrace>
 4. \<And>s. \<lbrakk>valid_fault f; (invs and Q and st_tcb_at active t and ex_nonz_cap_to t) s\<rbrakk> \<Longrightarrow> ?Q7 s proof (prove)
goal (4 subgoals):
 1. \<And>uu_ x. valid_fault f \<Longrightarrow> \<lbrace>?E9 uu_ x\<rbrace> set_thread_state t Inactive \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 2. \<And>uu_. valid_fault f \<Longrightarrow> \<lbrace>?B8 uu_\<rbrace> send_fault_ipc t f \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>, \<lbrace>?E9 uu_\<rbrace>
 3. valid_fault f \<Longrightarrow> \<lbrace>?Q7\<rbrace> gets_the (get_tcb t) \<lbrace>?B8\<rbrace>
 4. \<And>s. \<lbrakk>valid_fault f; (invs and Q and st_tcb_at active t and ex_nonz_cap_to t) s\<rbrakk> \<Longrightarrow> ?Q7 s proof (prove)
goal (3 subgoals):
 1. \<And>uu_. valid_fault f \<Longrightarrow> \<lbrace>?B8 uu_\<rbrace> send_fault_ipc t f \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>, \<lbrace>\<lambda>x s. (st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = tcb_st_refs_of Inactive) t and (\<lambda>s. \<not> halted Inactive \<longrightarrow> ex_nonz_cap_to t s) and (\<lambda>s. \<forall>a data. Inactive = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s) and (\<lambda>s. t \<noteq> idle_thread s) and (\<lambda>s. st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted Inactive \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) and (\<lambda>s. \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of Inactive) and (\<lambda>s. Inactive \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s) and K (Inactive \<noteq> IdleThreadState) and invs) s \<and> Q s\<rbrace>
 2. valid_fault f \<Longrightarrow> \<lbrace>?Q7\<rbrace> gets_the (get_tcb t) \<lbrace>?B8\<rbrace>
 3. \<And>s. \<lbrakk>valid_fault f; (invs and Q and st_tcb_at active t and ex_nonz_cap_to t) s\<rbrakk> \<Longrightarrow> ?Q7 s proof (prove)
goal (3 subgoals):
 1. \<And>uu_. valid_fault f \<Longrightarrow> \<lbrace>?B8 uu_\<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);
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))
odE \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>, \<lbrace>\<lambda>x s. st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s\<rbrace>
 2. valid_fault f \<Longrightarrow> \<lbrace>?Q7\<rbrace> gets_the (get_tcb t) \<lbrace>?B8\<rbrace>
 3. \<And>s. \<lbrakk>valid_fault f; (invs and Q and st_tcb_at active t and ex_nonz_cap_to t) s\<rbrakk> \<Longrightarrow> ?Q7 s proof (prove)
goal (4 subgoals):
 1. \<And>uu_ handler_cptr. valid_fault f \<Longrightarrow> \<lbrace>?P'488 uu_ handler_cptr\<rbrace> lookup_cap t handler_cptr \<lbrace>\<lambda>handler_cap s. (handler_cap = NullCap \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> ((\<exists>x xa xb xc. handler_cap = UntypedCap x xa xb xc) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> (\<forall>x xa xb. handler_cap = EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb) \<longrightarrow> invs s \<and> Q s \<and> st_tcb_at active t s \<and> ex_nonz_cap_to x s \<and> ex_nonz_cap_to t s) \<and> ((AllowSend \<in> xb \<longrightarrow> AllowGrant \<notin> xb \<and> AllowGrantReply \<notin> xb) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s)) \<and> ((\<exists>x xa xb. handler_cap = NotificationCap x xa xb) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> ((\<exists>x xa xb. handler_cap = ReplyCap x xa xb) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> ((\<exists>x xa xb. handler_cap = CNodeCap x xa xb) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> ((\<exists>x. handler_cap = ThreadCap x) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> (handler_cap = DomainCap \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> (handler_cap = IRQControlCap \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> ((\<exists>x. handler_cap = IRQHandlerCap x) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> ((\<exists>x xa xb. handler_cap = Zombie x xa xb) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> ((\<exists>x. handler_cap = ArchObjectCap x) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s)\<rbrace>, -
 2. \<And>uu_. valid_fault f \<Longrightarrow> \<lbrace>?B8 uu_\<rbrace> liftE (thread_get tcb_fault_handler t) \<lbrace>\<lambda>handler_cptr s. st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s \<and> ?P'488 uu_ handler_cptr s\<rbrace>, \<lbrace>\<lambda>x s. st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s\<rbrace>
 3. valid_fault f \<Longrightarrow> \<lbrace>?Q7\<rbrace> gets_the (get_tcb t) \<lbrace>?B8\<rbrace>
 4. \<And>s. \<lbrakk>valid_fault f; (invs and Q and st_tcb_at active t and ex_nonz_cap_to t) s\<rbrakk> \<Longrightarrow> ?Q7 s proof (prove)
goal (4 subgoals):
 1. \<And>uu_ handler_cptr. valid_fault f \<Longrightarrow> \<lbrace>?P'502 uu_ handler_cptr\<rbrace> lookup_cap t handler_cptr \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> ((\<exists>x xa xb xc. rv = UntypedCap x xa xb xc) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> (\<forall>x xa xb. rv = EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb) \<longrightarrow> invs s \<and> Q s \<and> st_tcb_at active t s \<and> ex_nonz_cap_to t s) \<and> ((AllowSend \<in> xb \<longrightarrow> AllowGrant \<notin> xb \<and> AllowGrantReply \<notin> xb) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s)) \<and> ((\<exists>x xa xb. rv = NotificationCap x xa xb) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> ((\<exists>x xa xb. rv = ReplyCap x xa xb) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> ((\<exists>x xa xb. rv = CNodeCap x xa xb) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> ((\<exists>x. rv = ThreadCap x) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> (rv = DomainCap \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> (rv = IRQControlCap \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> ((\<exists>x. rv = IRQHandlerCap x) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> ((\<exists>x xa xb. rv = Zombie x xa xb) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s) \<and> ((\<exists>x. rv = ArchObjectCap x) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s)\<rbrace>, -
 2. \<And>uu_. valid_fault f \<Longrightarrow> \<lbrace>?B8 uu_\<rbrace> liftE (thread_get tcb_fault_handler t) \<lbrace>\<lambda>handler_cptr s. st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s \<and> True \<and> ?P'502 uu_ handler_cptr s\<rbrace>, \<lbrace>\<lambda>x s. st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s \<and> invs s \<and> Q s\<rbrace>
 3. valid_fault f \<Longrightarrow> \<lbrace>?Q7\<rbrace> gets_the (get_tcb t) \<lbrace>?B8\<rbrace>
 4. \<And>s. \<lbrakk>valid_fault f; (invs and Q and st_tcb_at active t and ex_nonz_cap_to t) s\<rbrakk> \<Longrightarrow> ?Q7 s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>valid_fault f; invs s; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s \<and> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s \<and> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s \<and> ((\<exists>x. AllowSend \<in> x \<longrightarrow> AllowGrant \<notin> x \<and> AllowGrantReply \<notin> x) \<longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) \<and> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> t \<noteq> idle_thread s \<and> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>valid_fault f; invs s; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> valid_reply_caps s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s \<and> ((\<exists>x. AllowSend \<in> x \<longrightarrow> AllowGrant \<notin> x \<and> AllowGrantReply \<notin> x) \<longrightarrow> valid_reply_caps s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) t s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) proof (prove)
goal:
No subgoals!