theory Syscall_IF

lemma decode_invocation_authorised_globals_inv:
  "\<lbrace>invs and cte_wp_at ((=) cap) slot
         and (\<lambda>s :: det_state. \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s)\<rbrace>
   decode_invocation info_label args ptr slot cap excaps
   \<lbrace>authorised_for_globals_inv\<rbrace>, -" unfolding decode_invocation_def apply (rule hoare_pre) apply wpc apply ((wp authorised_for_globals_triv | wpc | simp add: uncurry_def)+)[11] apply (unfold authorised_for_globals_inv_def) apply wp apply (unfold comp_def) apply simp apply (wp decode_arch_invocation_authorised_for_globals) apply (intro impI conjI allI | clarsimp simp add: authorised_for_globals_inv_def)+ apply (erule_tac x="(a, aa, b)" in ballE) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s)\<rbrace> decode_invocation info_label args ptr slot cap excaps \<lbrace>authorised_for_globals_inv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s)\<rbrace> case cap of UntypedCap dev ptr sz fi \<Rightarrow> liftME InvokeUntyped $ decode_untyped_invocation info_label args slot cap (map fst excaps) | EndpointCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeEndpoint ptr badge (AllowGrant \<in> rights) (AllowGrantReply \<in> rights) else throwError $ InvalidCapability 0 | NotificationCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0 | ReplyCap thread True rights \<Rightarrow> throwError $ InvalidCapability 0 | ReplyCap thread False rights \<Rightarrow> returnOk $ InvokeReply thread slot (AllowGrant \<in> rights) | CNodeCap ptr bits x \<Rightarrow> liftME InvokeCNode $ decode_cnode_invocation info_label args cap (map fst excaps) | ThreadCap ptr \<Rightarrow> liftME InvokeTCB $ decode_tcb_invocation info_label args cap slot excaps | DomainCap \<Rightarrow> liftME (\<lambda>(x, y). InvokeDomain x y) $ decode_domain_invocation info_label args excaps | IRQControlCap \<Rightarrow> liftME InvokeIRQControl $ decode_irq_control_invocation info_label args slot (map fst excaps) | IRQHandlerCap irq \<Rightarrow> liftME InvokeIRQHandler $ decode_irq_handler_invocation info_label irq excaps | ArchObjectCap arch_cap \<Rightarrow> liftME InvokeArchObject $ arch_decode_invocation info_label args ptr slot arch_cap excaps | _ \<Rightarrow> throwError $ InvalidCapability 0 \<lbrace>authorised_for_globals_inv\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case cap of UntypedCap dev ptr sz fi \<Rightarrow> liftME InvokeUntyped $ decode_untyped_invocation info_label args slot cap (map fst excaps) | EndpointCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeEndpoint ptr badge (AllowGrant \<in> rights) (AllowGrantReply \<in> rights) else throwError $ InvalidCapability 0 | NotificationCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0 | ReplyCap thread True rights \<Rightarrow> throwError $ InvalidCapability 0 | ReplyCap thread False rights \<Rightarrow> returnOk $ InvokeReply thread slot (AllowGrant \<in> rights) | CNodeCap ptr bits x \<Rightarrow> liftME InvokeCNode $ decode_cnode_invocation info_label args cap (map fst excaps) | ThreadCap ptr \<Rightarrow> liftME InvokeTCB $ decode_tcb_invocation info_label args cap slot excaps | DomainCap \<Rightarrow> liftME (\<lambda>(x, y). InvokeDomain x y) $ decode_domain_invocation info_label args excaps | IRQControlCap \<Rightarrow> liftME InvokeIRQControl $ decode_irq_control_invocation info_label args slot (map fst excaps) | IRQHandlerCap irq \<Rightarrow> liftME InvokeIRQHandler $ decode_irq_handler_invocation info_label irq excaps | ArchObjectCap arch_cap \<Rightarrow> liftME InvokeArchObject $ arch_decode_invocation info_label args ptr slot arch_cap excaps | _ \<Rightarrow> throwError $ InvalidCapability 0 \<lbrace>authorised_for_globals_inv\<rbrace>, -
 2. \<And>s. (invs and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s)) s \<Longrightarrow> ?P' s proof (prove)
goal (13 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>?R52\<rbrace> throwError $ InvalidCapability 0 \<lbrace>authorised_for_globals_inv\<rbrace>, -
 2. \<And>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>?R53 x21 x22 x23 x24\<rbrace> liftME InvokeUntyped $ decode_untyped_invocation info_label args slot cap (map fst excaps) \<lbrace>authorised_for_globals_inv\<rbrace>, -
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>?R54 x31 x32 x33\<rbrace> if AllowSend \<in> x33 then returnOk $ InvokeEndpoint x31 x32 (AllowGrant \<in> x33) (AllowGrantReply \<in> x33) else throwError $ InvalidCapability 0 \<lbrace>authorised_for_globals_inv\<rbrace>, -
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>?R55 x41 x42 x43\<rbrace> if AllowSend \<in> x43 then returnOk $ InvokeNotification x41 x42 else throwError $ InvalidCapability 0 \<lbrace>authorised_for_globals_inv\<rbrace>, -
 5. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>?R56 x51 x52 x53\<rbrace> case x52 of True \<Rightarrow> throwError $ InvalidCapability 0 | False \<Rightarrow> returnOk $ InvokeReply x51 slot (AllowGrant \<in> x53) \<lbrace>authorised_for_globals_inv\<rbrace>, -
 6. \<And>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>?R57 x61 x62 x63\<rbrace> liftME InvokeCNode $ decode_cnode_invocation info_label args cap (map fst excaps) \<lbrace>authorised_for_globals_inv\<rbrace>, -
 7. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> \<lbrace>?R58 x7\<rbrace> liftME InvokeTCB $ decode_tcb_invocation info_label args cap slot excaps \<lbrace>authorised_for_globals_inv\<rbrace>, -
 8. cap = DomainCap \<Longrightarrow> \<lbrace>?R59\<rbrace> liftME (\<lambda>(x, y). InvokeDomain x y) $ decode_domain_invocation info_label args excaps \<lbrace>authorised_for_globals_inv\<rbrace>, -
 9. cap = IRQControlCap \<Longrightarrow> \<lbrace>?R60\<rbrace> liftME InvokeIRQControl $ decode_irq_control_invocation info_label args slot (map fst excaps) \<lbrace>authorised_for_globals_inv\<rbrace>, -
 10. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>?R61 x10\<rbrace> liftME InvokeIRQHandler $ decode_irq_handler_invocation info_label x10 excaps \<lbrace>authorised_for_globals_inv\<rbrace>, -
A total of 13 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>?R63 x12\<rbrace> liftME InvokeArchObject $ arch_decode_invocation info_label args ptr slot x12 excaps \<lbrace>authorised_for_globals_inv\<rbrace>, -
 2. \<And>s. (invs and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s)) s \<Longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> authorised_for_globals_inv (InvokeEndpoint x xa (AllowGrant \<in> xb) (AllowGrantReply \<in> xb)) s) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> authorised_for_globals_inv (InvokeNotification x xa) s) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> authorised_for_globals_inv (InvokeReply x slot (AllowGrant \<in> xb)) s)) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> True) \<and> (cap = DomainCap \<longrightarrow> True) \<and> (cap = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> ?R63 x s) proof (prove)
goal (2 subgoals):
 1. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>?R63 x12\<rbrace> liftME InvokeArchObject $ arch_decode_invocation info_label args ptr slot x12 excaps \<lbrace>\<lambda>oper s. case oper of InvokeArchObject ai \<Rightarrow> authorised_for_globals_arch_inv ai s | _ \<Rightarrow> True\<rbrace>, -
 2. \<And>s. (invs and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s)) s \<Longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> (case InvokeEndpoint x xa (AllowGrant \<in> xb) (AllowGrantReply \<in> xb) of InvokeArchObject ai \<Rightarrow> authorised_for_globals_arch_inv ai s | _ \<Rightarrow> True)) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> (case InvokeNotification x xa of InvokeArchObject ai \<Rightarrow> authorised_for_globals_arch_inv ai s | _ \<Rightarrow> True)) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> (case InvokeReply x slot (AllowGrant \<in> xb) of InvokeArchObject ai \<Rightarrow> authorised_for_globals_arch_inv ai s | _ \<Rightarrow> True))) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> True) \<and> (cap = DomainCap \<longrightarrow> True) \<and> (cap = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> ?R63 x s) proof (prove)
goal (2 subgoals):
 1. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>?R63 x12\<rbrace> arch_decode_invocation info_label args ptr slot x12 excaps \<lbrace>(\<lambda>oper s. case oper of InvokeArchObject ai \<Rightarrow> authorised_for_globals_arch_inv ai s | _ \<Rightarrow> True) \<circ> InvokeArchObject\<rbrace>, -
 2. \<And>s. (invs and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s)) s \<Longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> (case InvokeEndpoint x xa (AllowGrant \<in> xb) (AllowGrantReply \<in> xb) of InvokeArchObject ai \<Rightarrow> authorised_for_globals_arch_inv ai s | _ \<Rightarrow> True)) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> (case InvokeNotification x xa of InvokeArchObject ai \<Rightarrow> authorised_for_globals_arch_inv ai s | _ \<Rightarrow> True)) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> (case InvokeReply x slot (AllowGrant \<in> xb) of InvokeArchObject ai \<Rightarrow> authorised_for_globals_arch_inv ai s | _ \<Rightarrow> True))) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> True) \<and> (cap = DomainCap \<longrightarrow> True) \<and> (cap = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> ?R63 x s) proof (prove)
goal (2 subgoals):
 1. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>?R63 x12\<rbrace> arch_decode_invocation info_label args ptr slot x12 excaps \<lbrace>\<lambda>x s. case InvokeArchObject x of InvokeArchObject ai \<Rightarrow> authorised_for_globals_arch_inv ai s | _ \<Rightarrow> True\<rbrace>, -
 2. \<And>s. (invs and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s)) s \<Longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> (case InvokeEndpoint x xa (AllowGrant \<in> xb) (AllowGrantReply \<in> xb) of InvokeArchObject ai \<Rightarrow> authorised_for_globals_arch_inv ai s | _ \<Rightarrow> True)) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> (case InvokeNotification x xa of InvokeArchObject ai \<Rightarrow> authorised_for_globals_arch_inv ai s | _ \<Rightarrow> True)) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> (case InvokeReply x slot (AllowGrant \<in> xb) of InvokeArchObject ai \<Rightarrow> authorised_for_globals_arch_inv ai s | _ \<Rightarrow> True))) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> True) \<and> (cap = DomainCap \<longrightarrow> True) \<and> (cap = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> ?R63 x s) proof (prove)
goal (2 subgoals):
 1. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>?R63 x12\<rbrace> arch_decode_invocation info_label args ptr slot x12 excaps \<lbrace>authorised_for_globals_arch_inv\<rbrace>, -
 2. \<And>s. (invs and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s)) s \<Longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> (case InvokeEndpoint x xa (AllowGrant \<in> xb) (AllowGrantReply \<in> xb) of InvokeArchObject ai \<Rightarrow> authorised_for_globals_arch_inv ai s | _ \<Rightarrow> True)) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> (case InvokeNotification x xa of InvokeArchObject ai \<Rightarrow> authorised_for_globals_arch_inv ai s | _ \<Rightarrow> True)) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> (case InvokeReply x slot (AllowGrant \<in> xb) of InvokeArchObject ai \<Rightarrow> authorised_for_globals_arch_inv ai s | _ \<Rightarrow> True))) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> True) \<and> (cap = DomainCap \<longrightarrow> True) \<and> (cap = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> ?R63 x s) proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and cte_wp_at ((=) cap) slot and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s)) s \<Longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> (case InvokeEndpoint x xa (AllowGrant \<in> xb) (AllowGrantReply \<in> xb) of InvokeArchObject ai \<Rightarrow> authorised_for_globals_arch_inv ai s | _ \<Rightarrow> True)) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> (case InvokeNotification x xa of InvokeArchObject ai \<Rightarrow> authorised_for_globals_arch_inv ai s | _ \<Rightarrow> True)) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> (case InvokeReply x slot (AllowGrant \<in> xb) of InvokeArchObject ai \<Rightarrow> authorised_for_globals_arch_inv ai s | _ \<Rightarrow> True))) \<and> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> True) \<and> (cap = DomainCap \<longrightarrow> True) \<and> (cap = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. cap = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = ArchObjectCap x \<longrightarrow> (invs and cte_wp_at ((=) (ArchObjectCap x)) slot and (\<lambda>s. \<forall>(cap, slot)\<in>set excaps. cte_wp_at ((=) cap) slot s)) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x a aa b. \<lbrakk>cap = ArchObjectCap x; (a, aa, b) \<in> set excaps; invs s; cte_wp_at ((=) (ArchObjectCap x)) slot s; \<forall>x\<in>set excaps. cte_wp_at ((=) (fst x)) (snd x) s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) a) (aa, b) s proof (prove)
goal (2 subgoals):
 1. \<And>s x a aa b. \<lbrakk>cap = ArchObjectCap x; (a, aa, b) \<in> set excaps; invs s; cte_wp_at ((=) (ArchObjectCap x)) slot s; cte_wp_at ((=) (fst (a, aa, b))) (snd (a, aa, b)) s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) a) (aa, b) s
 2. \<And>s x a aa b. \<lbrakk>cap = ArchObjectCap x; (a, aa, b) \<in> set excaps; invs s; cte_wp_at ((=) (ArchObjectCap x)) slot s; (a, aa, b) \<notin> set excaps\<rbrakk> \<Longrightarrow> cte_wp_at ((=) a) (aa, b) s proof (prove)
goal:
No subgoals!