theory Ipc_IF

lemma send_fault_ipc_globals_equiv:
  "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs
                    and pspace_distinct and pspace_aligned and valid_global_objs
                    and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault fault)\<rbrace>
   send_fault_ipc tptr fault
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding send_fault_ipc_def apply (wp) apply (simp add: Let_def) apply (wp send_ipc_globals_equiv thread_set_globals_equiv thread_set_valid_objs''
               thread_set_fault_valid_global_refs thread_set_valid_idle_trivial thread_set_refs_trivial
            | wpc | simp)+ apply (rule_tac Q'="\<lambda>_. globals_equiv st and valid_objs and valid_arch_state and
                            valid_global_refs and pspace_distinct and pspace_aligned and
                            valid_global_objs and K (valid_fault fault) and valid_idle and
                            (\<lambda>s. sym_refs (state_refs_of s))" in hoare_post_imp_R) apply (wp | simp)+ apply (clarsimp) apply (rule valid_tcb_fault_update) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault fault)\<rbrace> send_fault_ipc tptr fault \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault fault)\<rbrace> doE handler_cptr <- liftE $ thread_get tcb_fault_handler tptr;
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tptr 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)) tptr;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tptr (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f
odE \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>handler_cptr handler_cap. \<lbrace>?B3 handler_cptr handler_cap\<rbrace> 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)) tptr;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tptr (cap_ep_ptr handler_cap)
od else throwError f | _ \<Rightarrow> throwError f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>handler_cptr. \<lbrace>?B2 handler_cptr\<rbrace> cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tptr handler_cptr \<lbrace>?B3 handler_cptr\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<lbrace>?Q\<rbrace> liftE $ thread_get tcb_fault_handler tptr \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault fault)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>handler_cptr handler_cap. \<lbrace>?B3 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 fault)) tptr;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True tptr (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>_. globals_equiv st\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>handler_cptr. \<lbrace>?B2 handler_cptr\<rbrace> cap_fault_on_failure (of_bl handler_cptr) False $ lookup_cap tptr handler_cptr \<lbrace>?B3 handler_cptr\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<lbrace>?Q\<rbrace> liftE $ thread_get tcb_fault_handler tptr \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault fault)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>handler_cptr. \<lbrace>?P'197 handler_cptr\<rbrace> lookup_cap tptr handler_cptr \<lbrace>\<lambda>handler_cap s. (handler_cap = NullCap \<longrightarrow> globals_equiv st s) \<and> ((\<exists>x xa xb xc. handler_cap = UntypedCap x xa xb xc) \<longrightarrow> globals_equiv st s) \<and> (\<forall>x xa xb. handler_cap = EndpointCap x xa xb \<longrightarrow> (AllowWrite \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb) \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> (\<forall>tcb. get_tcb tptr s = Some tcb \<longrightarrow> valid_tcb tptr tcb s \<longrightarrow> valid_tcb tptr (tcb\<lparr>tcb_fault := Some fault\<rparr>) s) \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> valid_idle s \<and> sym_refs (state_refs_of s)) \<and> ((AllowWrite \<in> xb \<longrightarrow> AllowGrant \<notin> xb \<and> AllowGrantReply \<notin> xb) \<longrightarrow> globals_equiv st s)) \<and> ((\<exists>x xa xb. handler_cap = NotificationCap x xa xb) \<longrightarrow> globals_equiv st s) \<and> ((\<exists>x xa xb. handler_cap = ReplyCap x xa xb) \<longrightarrow> globals_equiv st s) \<and> ((\<exists>x xa xb. handler_cap = CNodeCap x xa xb) \<longrightarrow> globals_equiv st s) \<and> ((\<exists>x. handler_cap = ThreadCap x) \<longrightarrow> globals_equiv st s) \<and> (handler_cap = DomainCap \<longrightarrow> globals_equiv st s) \<and> (handler_cap = IRQControlCap \<longrightarrow> globals_equiv st s) \<and> ((\<exists>x. handler_cap = IRQHandlerCap x) \<longrightarrow> globals_equiv st s) \<and> ((\<exists>x xa xb. handler_cap = Zombie x xa xb) \<longrightarrow> globals_equiv st s) \<and> ((\<exists>x. handler_cap = ArchObjectCap x) \<longrightarrow> globals_equiv st s)\<rbrace>, -
 2. \<lbrace>?Q\<rbrace> liftE $ thread_get tcb_fault_handler tptr \<lbrace>\<lambda>handler_cptr s. (globals_equiv st s \<and> True) \<and> ?P'197 handler_cptr s\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault fault)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>handler_cptr. \<lbrace>?P'197 handler_cptr\<rbrace> lookup_cap tptr handler_cptr \<lbrace>\<lambda>_. globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and K (valid_fault fault) and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))\<rbrace>, -
 2. \<And>handler_cptr rv s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and K (valid_fault fault) and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s \<Longrightarrow> (rv = NullCap \<longrightarrow> globals_equiv st s) \<and> ((\<exists>x xa xb xc. rv = UntypedCap x xa xb xc) \<longrightarrow> globals_equiv st s) \<and> (\<forall>x xa xb. rv = EndpointCap x xa xb \<longrightarrow> (AllowWrite \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb) \<longrightarrow> globals_equiv st s \<and> valid_arch_state s \<and> valid_objs s \<and> (\<forall>tcb. get_tcb tptr s = Some tcb \<longrightarrow> valid_tcb tptr tcb s \<longrightarrow> valid_tcb tptr (tcb\<lparr>tcb_fault := Some fault\<rparr>) s) \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> valid_idle s \<and> sym_refs (state_refs_of s)) \<and> ((AllowWrite \<in> xb \<longrightarrow> AllowGrant \<notin> xb \<and> AllowGrantReply \<notin> xb) \<longrightarrow> globals_equiv st s)) \<and> ((\<exists>x xa xb. rv = NotificationCap x xa xb) \<longrightarrow> globals_equiv st s) \<and> ((\<exists>x xa xb. rv = ReplyCap x xa xb) \<longrightarrow> globals_equiv st s) \<and> ((\<exists>x xa xb. rv = CNodeCap x xa xb) \<longrightarrow> globals_equiv st s) \<and> ((\<exists>x. rv = ThreadCap x) \<longrightarrow> globals_equiv st s) \<and> (rv = DomainCap \<longrightarrow> globals_equiv st s) \<and> (rv = IRQControlCap \<longrightarrow> globals_equiv st s) \<and> ((\<exists>x. rv = IRQHandlerCap x) \<longrightarrow> globals_equiv st s) \<and> ((\<exists>x xa xb. rv = Zombie x xa xb) \<longrightarrow> globals_equiv st s) \<and> ((\<exists>x. rv = ArchObjectCap x) \<longrightarrow> globals_equiv st s)
 3. \<lbrace>?Q\<rbrace> liftE $ thread_get tcb_fault_handler tptr \<lbrace>\<lambda>handler_cptr s. (globals_equiv st s \<and> True) \<and> ?P'197 handler_cptr s\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault fault)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. globals_equiv st s \<and> valid_objs s \<and> valid_arch_state s \<and> valid_global_refs s \<and> pspace_distinct s \<and> pspace_aligned s \<and> valid_global_objs s \<and> valid_fault fault \<and> valid_idle s \<and> sym_refs (state_refs_of s) \<Longrightarrow> \<forall>x xa xb. rv = EndpointCap x xa xb \<longrightarrow> AllowWrite \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb) \<longrightarrow> (\<forall>tcb. get_tcb tptr s = Some tcb \<longrightarrow> valid_tcb tptr tcb s \<longrightarrow> valid_tcb tptr (tcb\<lparr>tcb_fault := Some fault\<rparr>) s)
 2. \<lbrace>?Q\<rbrace> liftE $ thread_get tcb_fault_handler tptr \<lbrace>\<lambda>handler_cptr s. (globals_equiv st s \<and> True) \<and> (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and K (valid_fault fault) and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault fault)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>s xb tcb. \<lbrakk>globals_equiv st s; valid_objs s; valid_arch_state s; valid_global_refs s; pspace_distinct s; pspace_aligned s; valid_global_objs s; valid_fault fault; valid_idle s; sym_refs (state_refs_of s); AllowWrite \<in> xb; AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb; get_tcb tptr s = Some tcb; valid_tcb tptr tcb s\<rbrakk> \<Longrightarrow> valid_tcb tptr (tcb\<lparr>tcb_fault := Some fault\<rparr>) s
 2. \<lbrace>?Q\<rbrace> liftE $ thread_get tcb_fault_handler tptr \<lbrace>\<lambda>handler_cptr s. (globals_equiv st s \<and> True) \<and> (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and K (valid_fault fault) and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault fault)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>s xb tcb. \<lbrakk>globals_equiv st s; valid_objs s; valid_arch_state s; valid_global_refs s; pspace_distinct s; pspace_aligned s; valid_global_objs s; valid_fault fault; valid_idle s; sym_refs (state_refs_of s); AllowWrite \<in> xb; AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb; get_tcb tptr s = Some tcb; valid_tcb tptr tcb s\<rbrakk> \<Longrightarrow> valid_tcb tptr tcb s
 2. \<And>s xb tcb. \<lbrakk>globals_equiv st s; valid_objs s; valid_arch_state s; valid_global_refs s; pspace_distinct s; pspace_aligned s; valid_global_objs s; valid_fault fault; valid_idle s; sym_refs (state_refs_of s); AllowWrite \<in> xb; AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb; get_tcb tptr s = Some tcb; valid_tcb tptr tcb s\<rbrakk> \<Longrightarrow> valid_fault fault
 3. \<lbrace>?Q\<rbrace> liftE $ thread_get tcb_fault_handler tptr \<lbrace>\<lambda>handler_cptr s. (globals_equiv st s \<and> True) \<and> (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and K (valid_fault fault) and valid_idle and (\<lambda>s. sym_refs (state_refs_of s))) s\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<And>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault fault)) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!