theory DomainSepInv

lemma send_fault_ipc_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and valid_objs and sym_refs \<circ> state_refs_of
                           and valid_mdb and K (valid_fault fault)\<rbrace>
   send_fault_ipc thread fault
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>" unfolding send_fault_ipc_def apply (rule hoare_gen_asm)+ apply (wp send_ipc_domain_sep_inv thread_set_valid_objs thread_set_tcb_fault_update_valid_mdb
            thread_set_refs_trivial thread_set_obj_at_impossible hoare_vcg_ex_lift
         | wpc | simp add: Let_def split_def lookup_cap_def valid_tcb_fault_update)+ apply (wpe get_cap_inv[where P="domain_sep_inv irqs st and valid_objs and valid_mdb
                                                            and sym_refs o state_refs_of"]) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and valid_objs and sym_refs \<circ> state_refs_of and valid_mdb and K (valid_fault fault)\<rbrace> send_fault_ipc thread fault \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and valid_objs and sym_refs \<circ> state_refs_of and valid_mdb and K (valid_fault fault)\<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>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. valid_fault fault \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and valid_objs and sym_refs \<circ> state_refs_of and valid_mdb\<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>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>handler_cptr p. valid_fault fault \<Longrightarrow> \<lbrace>?B196 handler_cptr p\<rbrace> get_cap (fst p) \<lbrace>\<lambda>handler_cap s. (handler_cap = NullCap \<longrightarrow> domain_sep_inv irqs st s) \<and> ((\<exists>x xa xb xc. handler_cap = UntypedCap x xa xb xc) \<longrightarrow> domain_sep_inv irqs st 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> domain_sep_inv irqs st s \<and> valid_objs s \<and> valid_mdb s \<and> sym_refs (state_refs_of s)) \<and> ((AllowSend \<in> xb \<longrightarrow> AllowGrant \<notin> xb \<and> AllowGrantReply \<notin> xb) \<longrightarrow> domain_sep_inv irqs st s)) \<and> ((\<exists>x xa xb. handler_cap = NotificationCap x xa xb) \<longrightarrow> domain_sep_inv irqs st s) \<and> ((\<exists>x xa xb. handler_cap = ReplyCap x xa xb) \<longrightarrow> domain_sep_inv irqs st s) \<and> ((\<exists>x xa xb. handler_cap = CNodeCap x xa xb) \<longrightarrow> domain_sep_inv irqs st s) \<and> ((\<exists>x. handler_cap = ThreadCap x) \<longrightarrow> domain_sep_inv irqs st s) \<and> (handler_cap = DomainCap \<longrightarrow> domain_sep_inv irqs st s) \<and> (handler_cap = IRQControlCap \<longrightarrow> domain_sep_inv irqs st s) \<and> ((\<exists>x. handler_cap = IRQHandlerCap x) \<longrightarrow> domain_sep_inv irqs st s) \<and> ((\<exists>x xa xb. handler_cap = Zombie x xa xb) \<longrightarrow> domain_sep_inv irqs st s) \<and> ((\<exists>x. handler_cap = ArchObjectCap x) \<longrightarrow> domain_sep_inv irqs st s)\<rbrace>
 2. \<And>handler_cptr. valid_fault fault \<Longrightarrow> \<lbrace>?P'183 handler_cptr\<rbrace> lookup_slot_for_thread thread handler_cptr \<lbrace>?B196 handler_cptr\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. valid_fault fault \<Longrightarrow> \<lbrace>?Q2\<rbrace> liftE $ thread_get tcb_fault_handler thread \<lbrace>\<lambda>handler_cptr s. (domain_sep_inv irqs st s \<and> True) \<and> ?P'183 handler_cptr s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. \<And>s. \<lbrakk>valid_fault fault; (domain_sep_inv irqs st and valid_objs and sym_refs \<circ> state_refs_of and valid_mdb) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>handler_cptr p. valid_fault fault \<Longrightarrow> \<lbrace>?P'201 handler_cptr p\<rbrace> get_cap (fst p) \<lbrace>\<lambda>rv s. True\<rbrace>
 2. \<And>handler_cptr. valid_fault fault \<Longrightarrow> \<lbrace>?P'183 handler_cptr\<rbrace> lookup_slot_for_thread thread handler_cptr \<lbrace>\<lambda>p s. (domain_sep_inv irqs st and valid_objs and valid_mdb and sym_refs \<circ> state_refs_of) s \<and> ?P'201 handler_cptr p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. valid_fault fault \<Longrightarrow> \<lbrace>?Q2\<rbrace> liftE $ thread_get tcb_fault_handler thread \<lbrace>\<lambda>handler_cptr s. (domain_sep_inv irqs st s \<and> True) \<and> ?P'183 handler_cptr s\<rbrace>, \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. \<And>s. \<lbrakk>valid_fault fault; (domain_sep_inv irqs st and valid_objs and sym_refs \<circ> state_refs_of and valid_mdb) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal:
No subgoals!