theory DomainSepInv

lemma handle_recv_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and invs\<rbrace>
   handle_recv is_blocking
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>" apply (simp add: handle_recv_def Let_def lookup_cap_def split_def) apply (wp hoare_vcg_all_lift lookup_slot_for_thread_cap_fault receive_ipc_domain_sep_inv
            delete_caller_cap_domain_sep_inv get_cap_wp get_simple_ko_wp
         | wpc | simp
         | (rule_tac Q="\<lambda>rv. invs and (\<lambda>s. cur_thread s = thread)" in hoare_strengthen_post, wp,
            clarsimp simp: invs_valid_objs invs_sym_refs))+ apply (rule_tac Q'="\<lambda>r s. domain_sep_inv irqs st s \<and> invs s \<and>
                               tcb_at thread s \<and> thread = cur_thread s" in hoare_post_imp_R) apply wp apply ((clarsimp simp add: invs_valid_objs invs_sym_refs
             | intro impI allI conjI
             | rule cte_wp_valid_cap caps_of_state_cteD
             | fastforce simp:  valid_fault_def)+)[1] apply (wp delete_caller_cap_domain_sep_inv | simp add: split_def cong: conj_cong)+ apply (wp | simp add: invs_valid_objs invs_mdb invs_sym_refs tcb_at_invs)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and invs\<rbrace> handle_recv is_blocking \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and invs\<rbrace> do thread <- gets cur_thread;
ep_cptr <- liftM to_bl (as_user thread (getRegister cap_register));
cap_fault_on_failure (of_bl ep_cptr) True (doE ep_cap <- doE p <- lookup_slot_for_thread thread ep_cptr;
liftE (get_cap (fst p))
odE;
case ep_cap of EndpointCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then liftE $ do delete_caller_cap thread;
receive_ipc thread ep_cap is_blocking
od else throwError (MissingCapability 0) | NotificationCap ref badge rights \<Rightarrow> if AllowRecv \<in> rights then doE ntfn <- liftE $ get_notification ref;
boundTCB <- returnOk $ ntfn_bound_tcb ntfn;
if boundTCB = Some thread \<or> boundTCB = None then liftE $ receive_signal thread ep_cap is_blocking else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) | _ \<Rightarrow> throwError (MissingCapability 0)
odE) <catch> handle_fault thread
od \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>thread ep_cptr. \<lbrace>?P'291 thread ep_cptr\<rbrace> lookup_slot_for_thread thread ep_cptr \<lbrace>\<lambda>p s. \<forall>cap. cte_wp_at ((=) cap) (fst p) s \<longrightarrow> (cap = NullCap \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> ((\<exists>x xa xb xc. cap = UntypedCap x xa xb xc) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowRecv \<in> xb \<longrightarrow> domain_sep_inv irqs st s \<and> invs s \<and> tcb_at thread s \<and> cur_thread s = thread) \<and> (AllowRecv \<notin> xb \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (AllowRecv \<in> xb \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) x s \<longrightarrow> (ntfn_bound_tcb ntfn = Some thread \<longrightarrow> domain_sep_inv irqs st s) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> domain_sep_inv irqs st s) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))) \<and> (AllowRecv \<notin> xb \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> ((\<exists>x xa xb. cap = ReplyCap x xa xb) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> ((\<exists>x xa xb. cap = CNodeCap x xa xb) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> ((\<exists>x. cap = ThreadCap x) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> (cap = DomainCap \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> (cap = IRQControlCap \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> ((\<exists>x. cap = IRQHandlerCap x) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> ((\<exists>x xa xb. cap = Zombie x xa xb) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> ((\<exists>x. cap = ArchObjectCap x) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))\<rbrace>, -
 2. \<And>thread. \<lbrace>?B1 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. domain_sep_inv irqs st s \<and> (valid_objs and sym_refs \<circ> state_refs_of and valid_mdb) s \<and> invs s \<and> ?P'291 thread ep_cptr s\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 4. \<And>s. (domain_sep_inv irqs st and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>thread ep_cptr. \<lbrace>?P'291 thread ep_cptr\<rbrace> lookup_slot_for_thread thread ep_cptr \<lbrace>\<lambda>r s. domain_sep_inv irqs st s \<and> invs s \<and> tcb_at thread s \<and> thread = cur_thread s\<rbrace>, -
 2. \<And>thread ep_cptr rv s. domain_sep_inv irqs st s \<and> invs s \<and> tcb_at thread s \<and> thread = cur_thread s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (fst rv) s \<longrightarrow> (cap = NullCap \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> ((\<exists>x xa xb xc. cap = UntypedCap x xa xb xc) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowRecv \<in> xb \<longrightarrow> domain_sep_inv irqs st s \<and> invs s \<and> tcb_at thread s \<and> cur_thread s = thread) \<and> (AllowRecv \<notin> xb \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (AllowRecv \<in> xb \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) x s \<longrightarrow> (ntfn_bound_tcb ntfn = Some thread \<longrightarrow> domain_sep_inv irqs st s) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> domain_sep_inv irqs st s) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))) \<and> (AllowRecv \<notin> xb \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> ((\<exists>x xa xb. cap = ReplyCap x xa xb) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> ((\<exists>x xa xb. cap = CNodeCap x xa xb) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> ((\<exists>x. cap = ThreadCap x) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> (cap = DomainCap \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> (cap = IRQControlCap \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> ((\<exists>x. cap = IRQHandlerCap x) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> ((\<exists>x xa xb. cap = Zombie x xa xb) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> ((\<exists>x. cap = ArchObjectCap x) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))
 3. \<And>thread. \<lbrace>?B1 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. domain_sep_inv irqs st s \<and> (valid_objs and sym_refs \<circ> state_refs_of and valid_mdb) s \<and> invs s \<and> ?P'291 thread ep_cptr s\<rbrace>
 4. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 5. \<And>s. (domain_sep_inv irqs st and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>thread ep_cptr rv s. domain_sep_inv irqs st s \<and> invs s \<and> tcb_at thread s \<and> thread = cur_thread s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (fst rv) s \<longrightarrow> (cap = NullCap \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> ((\<exists>x xa xb xc. cap = UntypedCap x xa xb xc) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowRecv \<in> xb \<longrightarrow> domain_sep_inv irqs st s \<and> invs s \<and> tcb_at thread s \<and> cur_thread s = thread) \<and> (AllowRecv \<notin> xb \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (AllowRecv \<in> xb \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) x s \<longrightarrow> (ntfn_bound_tcb ntfn = Some thread \<longrightarrow> domain_sep_inv irqs st s) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> domain_sep_inv irqs st s) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))) \<and> (AllowRecv \<notin> xb \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> ((\<exists>x xa xb. cap = ReplyCap x xa xb) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> ((\<exists>x xa xb. cap = CNodeCap x xa xb) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> ((\<exists>x. cap = ThreadCap x) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> (cap = DomainCap \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> (cap = IRQControlCap \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> ((\<exists>x. cap = IRQHandlerCap x) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> ((\<exists>x xa xb. cap = Zombie x xa xb) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))) \<and> ((\<exists>x. cap = ArchObjectCap x) \<longrightarrow> domain_sep_inv irqs st s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))
 2. \<And>thread. \<lbrace>?B1 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. domain_sep_inv irqs st s \<and> (valid_objs and sym_refs \<circ> state_refs_of and valid_mdb) s \<and> invs s \<and> domain_sep_inv irqs st s \<and> invs s \<and> tcb_at thread s \<and> thread = cur_thread s\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 4. \<And>s. (domain_sep_inv irqs st and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>?B1 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. domain_sep_inv irqs st s \<and> (valid_objs and sym_refs \<circ> state_refs_of and valid_mdb) s \<and> invs s \<and> domain_sep_inv irqs st s \<and> invs s \<and> tcb_at thread s \<and> thread = cur_thread s\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 3. \<And>s. (domain_sep_inv irqs st and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. domain_sep_inv irqs st s \<and> invs s \<Longrightarrow> valid_objs s \<and> sym_refs (state_refs_of s) \<and> valid_mdb s \<and> tcb_at (cur_thread s) s proof (prove)
goal:
No subgoals!