theory FinalCaps

lemma send_fault_ipc_silc_inv:
  "\<lbrace>pas_refined aag and invs and is_subject aag \<circ> cur_thread and silc_inv aag st
                    and K (valid_fault fault \<and> is_subject aag thread)\<rbrace>
   send_fault_ipc thread fault
   \<lbrace>\<lambda>rv. silc_inv aag st\<rbrace>" apply (rule hoare_gen_asm)+ unfolding send_fault_ipc_def apply (wp send_ipc_silc_inv  thread_set_tcb_fault_set_invs
            thread_set_fault_pas_refined thread_set_refs_trivial thread_set_obj_at_impossible
            hoare_vcg_ex_lift get_cap_wp hoare_vcg_conj_lift hoare_vcg_ex_lift hoare_vcg_all_lift
         | wpc
         | simp add: Let_def split_def lookup_cap_def valid_tcb_fault_update)+ apply (rule_tac Q'="\<lambda>rv s. silc_inv aag st s \<and> pas_refined aag s
                             \<and> is_subject aag (cur_thread s)
                             \<and> invs s
                             \<and> valid_fault fault
                             \<and> is_subject aag (fst (fst rv))"
                 in hoare_post_imp_R[rotated]) apply (force dest!: cap_auth_caps_of_state
                   simp: invs_valid_objs invs_sym_refs cte_wp_at_caps_of_state aag_cap_auth_def
                         cap_auth_conferred_def cap_rights_to_auth_def) apply (wp get_cap_auth_wp[where aag=aag] lookup_slot_for_thread_authorised
          | simp add: add: lookup_cap_def split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and is_subject aag \<circ> cur_thread and silc_inv aag st and K (valid_fault fault \<and> is_subject aag thread)\<rbrace> send_fault_ipc thread fault \<lbrace>\<lambda>rv. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. valid_fault fault \<and> is_subject aag thread \<Longrightarrow> \<lbrace>pas_refined aag and invs and is_subject aag \<circ> cur_thread and silc_inv aag st\<rbrace> send_fault_ipc thread fault \<lbrace>\<lambda>rv. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. valid_fault fault \<and> is_subject aag thread \<Longrightarrow> \<lbrace>pas_refined aag and invs and is_subject aag \<circ> cur_thread and silc_inv aag st\<rbrace> doE handler_cptr <- liftE $ thread_get tcb_fault_handler thread;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap thread handler_cptr;
let f = 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 fault)) thread;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE \<lbrace>\<lambda>rv. silc_inv aag st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>handler_cptr. valid_fault fault \<and> is_subject aag thread \<Longrightarrow> \<lbrace>?P'200 handler_cptr\<rbrace> lookup_slot_for_thread thread handler_cptr \<lbrace>\<lambda>p s. \<forall>cap. cte_wp_at ((=) cap) (fst p) s \<longrightarrow> (cap = NullCap \<longrightarrow> silc_inv aag st s) \<and> ((\<exists>x xa xb xc. cap = UntypedCap x xa xb xc) \<longrightarrow> silc_inv aag st s) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowWrite \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (AllowGrant \<in> xb \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag x) \<in> pasPolicy aag)) \<and> ((AllowWrite \<in> xb \<longrightarrow> AllowGrant \<notin> xb \<and> AllowGrantReply \<notin> xb) \<longrightarrow> silc_inv aag st s)) \<and> ((\<exists>x xa xb. cap = NotificationCap x xa xb) \<longrightarrow> silc_inv aag st s) \<and> ((\<exists>x xa xb. cap = ReplyCap x xa xb) \<longrightarrow> silc_inv aag st s) \<and> ((\<exists>x xa xb. cap = CNodeCap x xa xb) \<longrightarrow> silc_inv aag st s) \<and> ((\<exists>x. cap = ThreadCap x) \<longrightarrow> silc_inv aag st s) \<and> (cap = DomainCap \<longrightarrow> silc_inv aag st s) \<and> (cap = IRQControlCap \<longrightarrow> silc_inv aag st s) \<and> ((\<exists>x. cap = IRQHandlerCap x) \<longrightarrow> silc_inv aag st s) \<and> ((\<exists>x xa xb. cap = Zombie x xa xb) \<longrightarrow> silc_inv aag st s) \<and> ((\<exists>x. cap = ArchObjectCap x) \<longrightarrow> silc_inv aag st s)\<rbrace>, -
 2. valid_fault fault \<and> is_subject aag thread \<Longrightarrow> \<lbrace>?Q2\<rbrace> liftE $ thread_get tcb_fault_handler thread \<lbrace>\<lambda>handler_cptr s. (silc_inv aag st s \<and> True) \<and> True \<and> ?P'200 handler_cptr s\<rbrace>, \<lbrace>\<lambda>rv. silc_inv aag st\<rbrace>
 3. \<And>s. \<lbrakk>valid_fault fault \<and> is_subject aag thread; (pas_refined aag and invs and is_subject aag \<circ> cur_thread and silc_inv aag st) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>handler_cptr rv s. \<lbrakk>valid_fault fault \<and> is_subject aag thread; silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> invs s \<and> valid_fault fault \<and> is_subject aag (fst (fst rv))\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (fst rv) s \<longrightarrow> (cap = NullCap \<longrightarrow> silc_inv aag st s) \<and> ((\<exists>x xa xb xc. cap = UntypedCap x xa xb xc) \<longrightarrow> silc_inv aag st s) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowWrite \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb) \<longrightarrow> silc_inv aag st s \<and> invs s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (AllowGrant \<in> xb \<longrightarrow> (pasSubject aag, Grant, pasObjectAbs aag x) \<in> pasPolicy aag)) \<and> ((AllowWrite \<in> xb \<longrightarrow> AllowGrant \<notin> xb \<and> AllowGrantReply \<notin> xb) \<longrightarrow> silc_inv aag st s)) \<and> ((\<exists>x xa xb. cap = NotificationCap x xa xb) \<longrightarrow> silc_inv aag st s) \<and> ((\<exists>x xa xb. cap = ReplyCap x xa xb) \<longrightarrow> silc_inv aag st s) \<and> ((\<exists>x xa xb. cap = CNodeCap x xa xb) \<longrightarrow> silc_inv aag st s) \<and> ((\<exists>x. cap = ThreadCap x) \<longrightarrow> silc_inv aag st s) \<and> (cap = DomainCap \<longrightarrow> silc_inv aag st s) \<and> (cap = IRQControlCap \<longrightarrow> silc_inv aag st s) \<and> ((\<exists>x. cap = IRQHandlerCap x) \<longrightarrow> silc_inv aag st s) \<and> ((\<exists>x xa xb. cap = Zombie x xa xb) \<longrightarrow> silc_inv aag st s) \<and> ((\<exists>x. cap = ArchObjectCap x) \<longrightarrow> silc_inv aag st s)
 2. \<And>handler_cptr. valid_fault fault \<and> is_subject aag thread \<Longrightarrow> \<lbrace>?P'200 handler_cptr\<rbrace> lookup_slot_for_thread thread handler_cptr \<lbrace>\<lambda>rv s. silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> invs s \<and> valid_fault fault \<and> is_subject aag (fst (fst rv))\<rbrace>, -
 3. valid_fault fault \<and> is_subject aag thread \<Longrightarrow> \<lbrace>?Q2\<rbrace> liftE $ thread_get tcb_fault_handler thread \<lbrace>\<lambda>handler_cptr s. (silc_inv aag st s \<and> True) \<and> True \<and> ?P'200 handler_cptr s\<rbrace>, \<lbrace>\<lambda>rv. silc_inv aag st\<rbrace>
 4. \<And>s. \<lbrakk>valid_fault fault \<and> is_subject aag thread; (pas_refined aag and invs and is_subject aag \<circ> cur_thread and silc_inv aag st) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>handler_cptr. valid_fault fault \<and> is_subject aag thread \<Longrightarrow> \<lbrace>?P'200 handler_cptr\<rbrace> lookup_slot_for_thread thread handler_cptr \<lbrace>\<lambda>rv s. silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> invs s \<and> valid_fault fault \<and> is_subject aag (fst (fst rv))\<rbrace>, -
 2. valid_fault fault \<and> is_subject aag thread \<Longrightarrow> \<lbrace>?Q2\<rbrace> liftE $ thread_get tcb_fault_handler thread \<lbrace>\<lambda>handler_cptr s. (silc_inv aag st s \<and> True) \<and> True \<and> ?P'200 handler_cptr s\<rbrace>, \<lbrace>\<lambda>rv. silc_inv aag st\<rbrace>
 3. \<And>s. \<lbrakk>valid_fault fault \<and> is_subject aag thread; (pas_refined aag and invs and is_subject aag \<circ> cur_thread and silc_inv aag st) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal:
No subgoals!