theory Ipc_AC

lemma handle_fault_pas_refined:
  "\<lbrace>pas_refined aag and invs and is_subject aag \<circ> cur_thread
                    and K (valid_fault fault) and K (is_subject aag thread)\<rbrace>
   handle_fault thread fault
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (wpsimp wp: set_thread_state_pas_refined simp: handle_fault_def handle_double_fault_def) apply (rule hoare_vcg_E_elim) apply (clarsimp simp: send_fault_ipc_def Let_def) apply wp apply wpsimp apply (rule hoare_post_impErr[where E=E and F=E for E]) apply (rule valid_validE) apply (wpsimp wp: send_fault_ipc_pas_refined)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and is_subject aag \<circ> cur_thread and K (valid_fault fault) and K (is_subject aag thread)\<rbrace> handle_fault thread fault \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>uu_. \<lbrace>?B2 uu_\<rbrace> send_fault_ipc thread fault \<lbrace>\<lambda>_. pas_refined aag\<rbrace>, \<lbrace>\<lambda>x s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s\<rbrace>
 2. \<lbrace>?Q1\<rbrace> gets_the (get_tcb thread) \<lbrace>?B2\<rbrace>
 3. \<And>s. (pas_refined aag and invs and is_subject aag \<circ> cur_thread and (\<lambda>y. valid_fault fault) and (\<lambda>y. is_subject aag thread)) s \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<And>uu_. \<lbrace>?P18 uu_\<rbrace> send_fault_ipc thread fault -, \<lbrace>\<lambda>x s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s\<rbrace>
 2. \<And>uu_. \<lbrace>?P'18 uu_\<rbrace> send_fault_ipc thread fault \<lbrace>\<lambda>_. pas_refined aag\<rbrace>, -
 3. \<lbrace>?Q1\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>uu_ s. ?P18 uu_ s \<and> ?P'18 uu_ s\<rbrace>
 4. \<And>s. (pas_refined aag and invs and is_subject aag \<circ> cur_thread and (\<lambda>y. valid_fault fault) and (\<lambda>y. is_subject aag thread)) s \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<And>uu_. \<lbrace>?P18 uu_\<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);
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 (CapFault (of_bl handler_cptr) False (MissingCapability 0)) | _ \<Rightarrow> throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0))
odE -, \<lbrace>\<lambda>x s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s\<rbrace>
 2. \<And>uu_. \<lbrace>?P'18 uu_\<rbrace> send_fault_ipc thread fault \<lbrace>\<lambda>_. pas_refined aag\<rbrace>, -
 3. \<lbrace>?Q1\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>uu_ s. ?P18 uu_ s \<and> ?P'18 uu_ s\<rbrace>
 4. \<And>s. (pas_refined aag and invs and is_subject aag \<circ> cur_thread and (\<lambda>y. valid_fault fault) and (\<lambda>y. is_subject aag thread)) s \<Longrightarrow> ?Q1 s proof (prove)
goal (6 subgoals):
 1. \<And>uu_ handler_cptr handler_cap. \<lbrace>?B25 uu_ 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)) thread;
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> rights) True thread (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>x s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s\<rbrace>
 2. \<And>uu_ handler_cptr. \<lbrace>?B24 uu_ handler_cptr\<rbrace> cap_fault_on_failure (of_bl handler_cptr) False (lookup_cap thread handler_cptr) \<lbrace>?B25 uu_ handler_cptr\<rbrace>, \<lbrace>\<lambda>x s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s\<rbrace>
 3. \<And>uu_. \<lbrace>?P18 uu_\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>?B24 uu_\<rbrace>, \<lbrace>\<lambda>x s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s\<rbrace>
 4. \<And>uu_. \<lbrace>?P'18 uu_\<rbrace> send_fault_ipc thread fault \<lbrace>\<lambda>_. pas_refined aag\<rbrace>, -
 5. \<lbrace>?Q1\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>uu_ s. ?P18 uu_ s \<and> ?P'18 uu_ s\<rbrace>
 6. \<And>s. (pas_refined aag and invs and is_subject aag \<circ> cur_thread and (\<lambda>y. valid_fault fault) and (\<lambda>y. is_subject aag thread)) s \<Longrightarrow> ?Q1 s proof (prove)
goal (5 subgoals):
 1. \<And>uu_ handler_cptr. \<lbrace>?B24 uu_ handler_cptr\<rbrace> cap_fault_on_failure (of_bl handler_cptr) False (lookup_cap thread handler_cptr) \<lbrace>\<lambda>handler_cap s. (handler_cap = NullCap \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x xa xb xc. handler_cap = UntypedCap x xa xb xc \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state 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> True) \<and> (\<not> (AllowSend \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb)) \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) \<and> (\<forall>x xa xb. handler_cap = NotificationCap x xa xb \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x xa xb. handler_cap = ReplyCap x xa xb \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x xa xb. handler_cap = CNodeCap x xa xb \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x. handler_cap = ThreadCap x \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (handler_cap = DomainCap \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (handler_cap = IRQControlCap \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x. handler_cap = IRQHandlerCap x \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x xa xb. handler_cap = Zombie x xa xb \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x. handler_cap = ArchObjectCap x \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)\<rbrace>, \<lbrace>\<lambda>x s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s\<rbrace>
 2. \<And>uu_. \<lbrace>?P18 uu_\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>?B24 uu_\<rbrace>, \<lbrace>\<lambda>x s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s\<rbrace>
 3. \<And>uu_. \<lbrace>?P'18 uu_\<rbrace> send_fault_ipc thread fault \<lbrace>\<lambda>_. pas_refined aag\<rbrace>, -
 4. \<lbrace>?Q1\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>uu_ s. ?P18 uu_ s \<and> ?P'18 uu_ s\<rbrace>
 5. \<And>s. (pas_refined aag and invs and is_subject aag \<circ> cur_thread and (\<lambda>y. valid_fault fault) and (\<lambda>y. is_subject aag thread)) s \<Longrightarrow> ?Q1 s proof (prove)
goal (7 subgoals):
 1. \<And>uu_ handler_cptr. \<lbrace>?B24 uu_ handler_cptr\<rbrace> cap_fault_on_failure (of_bl handler_cptr) False (lookup_cap thread handler_cptr) \<lbrace>?Q142 uu_ handler_cptr\<rbrace>, \<lbrace>\<lambda>x s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s\<rbrace>
 2. \<And>uu_ handler_cptr rv s. ?Q142 uu_ handler_cptr rv s \<Longrightarrow> (rv = NullCap \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x xa xb xc. rv = UntypedCap x xa xb xc \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x xa xb. rv = EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb) \<longrightarrow> True) \<and> (\<not> (AllowSend \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb)) \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) \<and> (\<forall>x xa xb. rv = NotificationCap x xa xb \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x xa xb. rv = ReplyCap x xa xb \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x xa xb. rv = CNodeCap x xa xb \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x. rv = ThreadCap x \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (rv = DomainCap \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (rv = IRQControlCap \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x. rv = IRQHandlerCap x \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x xa xb. rv = Zombie x xa xb \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x. rv = ArchObjectCap x \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)
 3. \<And>_ handler_cptr e s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<Longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s
 4. \<And>uu_. \<lbrace>?P18 uu_\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>?B24 uu_\<rbrace>, \<lbrace>\<lambda>x s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s\<rbrace>
 5. \<And>uu_. \<lbrace>?P'18 uu_\<rbrace> send_fault_ipc thread fault \<lbrace>\<lambda>_. pas_refined aag\<rbrace>, -
 6. \<lbrace>?Q1\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>uu_ s. ?P18 uu_ s \<and> ?P'18 uu_ s\<rbrace>
 7. \<And>s. (pas_refined aag and invs and is_subject aag \<circ> cur_thread and (\<lambda>y. valid_fault fault) and (\<lambda>y. is_subject aag thread)) s \<Longrightarrow> ?Q1 s proof (prove)
goal (7 subgoals):
 1. \<And>uu_ handler_cptr. \<lbrace>?B24 uu_ handler_cptr\<rbrace> cap_fault_on_failure (of_bl handler_cptr) False (lookup_cap thread handler_cptr) \<lbrace>\<lambda>x s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s\<rbrace>
 2. \<And>_ handler_cptr rv s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<Longrightarrow> (rv = NullCap \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x xa xb xc. rv = UntypedCap x xa xb xc \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x xa xb. rv = EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb) \<longrightarrow> True) \<and> (\<not> (AllowSend \<in> xb \<and> (AllowGrant \<in> xb \<or> AllowGrantReply \<in> xb)) \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) \<and> (\<forall>x xa xb. rv = NotificationCap x xa xb \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x xa xb. rv = ReplyCap x xa xb \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x xa xb. rv = CNodeCap x xa xb \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x. rv = ThreadCap x \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (rv = DomainCap \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (rv = IRQControlCap \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x. rv = IRQHandlerCap x \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x xa xb. rv = Zombie x xa xb \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> (\<forall>x. rv = ArchObjectCap x \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)
 3. \<And>_ handler_cptr e s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<Longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s
 4. \<And>uu_. \<lbrace>?P18 uu_\<rbrace> liftE (thread_get tcb_fault_handler thread) \<lbrace>?B24 uu_\<rbrace>, \<lbrace>\<lambda>x s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s\<rbrace>
 5. \<And>uu_. \<lbrace>?P'18 uu_\<rbrace> send_fault_ipc thread fault \<lbrace>\<lambda>_. pas_refined aag\<rbrace>, -
 6. \<lbrace>?Q1\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>uu_ s. ?P18 uu_ s \<and> ?P'18 uu_ s\<rbrace>
 7. \<And>s. (pas_refined aag and invs and is_subject aag \<circ> cur_thread and (\<lambda>y. valid_fault fault) and (\<lambda>y. is_subject aag thread)) s \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>pas_refined aag s; invs s; is_subject aag (cur_thread s); valid_fault fault; is_subject aag thread; get_tcb thread s = Some y\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s proof (prove)
goal:
No subgoals!