theory Syscall_S

lemma decode_separate_inv:
  "\<lbrace>\<top> and K ((\<forall>c \<in> set f. separate_cap (fst c)) \<and> (separate_cap cap))\<rbrace> Decode_A.decode_invocation a b c d cap f  \<lbrace>\<lambda>rv s. separate_inv rv\<rbrace>, -" unfolding Decode_A.decode_invocation_def apply (rule hoare_gen_asmE) apply clarify apply (erule separate_capE, simp_all split del: if_split) apply (rule hoare_pre, (wp | simp add: comp_def)+)[1] apply (rule hoare_pre) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>_. True) and K ((\<forall>c\<in>set f. separate_cap (fst c)) \<and> separate_cap cap)\<rbrace> Decode_A.decode_invocation a b c d cap f \<lbrace>\<lambda>rv s. separate_inv rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>_. True) and K ((\<forall>c\<in>set f. separate_cap (fst c)) \<and> separate_cap cap)\<rbrace> case cap of UntypedCap dev ptr sz fi \<Rightarrow> liftME InvokeUntyped $ decode_untyped_invocation a b d cap (map fst f) | 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 d (AllowGrant \<in> rights) | CNodeCap ptr bits x \<Rightarrow> liftME InvokeCNode $ decode_cnode_invocation a b cap (map fst f) | ThreadCap ptr \<Rightarrow> liftME InvokeTCB $ decode_tcb_invocation a b cap d f | DomainCap \<Rightarrow> liftME (\<lambda>(x, y). InvokeDomain x y) $ decode_domain_invocation a b f | IRQControlCap \<Rightarrow> liftME InvokeIRQControl $ decode_irq_control_invocation a b d (map fst f) | IRQHandlerCap irq \<Rightarrow> liftME InvokeIRQHandler $ decode_irq_handler_invocation a irq f | ArchObjectCap arch_cap \<Rightarrow> liftME InvokeArchObject $ arch_decode_invocation a b c d arch_cap f | _ \<Rightarrow> throwError $ InvalidCapability 0 \<lbrace>\<lambda>rv s. separate_inv rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. (\<forall>c\<in>set f. separate_cap (fst c)) \<and> separate_cap cap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case cap of UntypedCap dev ptr sz fi \<Rightarrow> liftME InvokeUntyped $ decode_untyped_invocation a b d cap (map fst f) | 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 d (AllowGrant \<in> rights) | CNodeCap ptr bits x \<Rightarrow> liftME InvokeCNode $ decode_cnode_invocation a b cap (map fst f) | ThreadCap ptr \<Rightarrow> liftME InvokeTCB $ decode_tcb_invocation a b cap d f | DomainCap \<Rightarrow> liftME (\<lambda>(x, y). InvokeDomain x y) $ decode_domain_invocation a b f | IRQControlCap \<Rightarrow> liftME InvokeIRQControl $ decode_irq_control_invocation a b d (map fst f) | IRQHandlerCap irq \<Rightarrow> liftME InvokeIRQHandler $ decode_irq_handler_invocation a irq f | ArchObjectCap arch_cap \<Rightarrow> liftME InvokeArchObject $ arch_decode_invocation a b c d arch_cap f | _ \<Rightarrow> throwError $ InvalidCapability 0 \<lbrace>\<lambda>rv s. separate_inv rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>c\<in>set f. separate_cap (fst c); separate_cap cap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case cap of UntypedCap dev ptr sz fi \<Rightarrow> liftME InvokeUntyped $ decode_untyped_invocation a b d cap (map fst f) | 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 d (AllowGrant \<in> rights) | CNodeCap ptr bits x \<Rightarrow> liftME InvokeCNode $ decode_cnode_invocation a b cap (map fst f) | ThreadCap ptr \<Rightarrow> liftME InvokeTCB $ decode_tcb_invocation a b cap d f | DomainCap \<Rightarrow> liftME (\<lambda>(x, y). InvokeDomain x y) $ decode_domain_invocation a b f | IRQControlCap \<Rightarrow> liftME InvokeIRQControl $ decode_irq_control_invocation a b d (map fst f) | IRQHandlerCap irq \<Rightarrow> liftME InvokeIRQHandler $ decode_irq_handler_invocation a irq f | ArchObjectCap arch_cap \<Rightarrow> liftME InvokeArchObject $ arch_decode_invocation a b c d arch_cap f | _ \<Rightarrow> throwError $ InvalidCapability 0 \<lbrace>\<lambda>rv s. separate_inv rv\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>c\<in>set f. separate_cap (fst c); cap = NullCap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> throwError (InvalidCapability 0) \<lbrace>\<lambda>rv s. separate_inv rv\<rbrace>, -
 2. \<And>ptr badge rights. \<lbrakk>\<forall>c\<in>set f. separate_cap (fst c); cap = NotificationCap ptr badge rights\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> if AllowSend \<in> rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0 \<lbrace>\<lambda>rv s. separate_inv rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>ptr badge rights. \<lbrakk>\<forall>c\<in>set f. separate_cap (fst c); cap = NotificationCap ptr badge rights\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> if AllowSend \<in> rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0 \<lbrace>\<lambda>rv s. separate_inv rv\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>ptr badge rights. \<lbrakk>\<forall>c\<in>set f. separate_cap (fst c); cap = NotificationCap ptr badge rights\<rbrakk> \<Longrightarrow> \<lbrace>?P'15 ptr badge rights\<rbrace> if AllowSend \<in> rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0 \<lbrace>\<lambda>rv s. separate_inv rv\<rbrace>, -
 2. \<And>ptr badge rights s. \<lbrakk>\<forall>c\<in>set f. separate_cap (fst c); cap = NotificationCap ptr badge rights; True\<rbrakk> \<Longrightarrow> ?P'15 ptr badge rights s proof (prove)
goal:
No subgoals!