theory Syscall_S

lemma decode_invocation_bisim:
  "bisim ((=) \<oplus> (=)) \<top> (K (separate_cap cap))
     (decode_invocation a b c d cap f) (Decode_A.decode_invocation a b c d cap f)" unfolding decode_invocation_def Decode_A.decode_invocation_def apply (rule bisim_guard_imp) apply (rule bisim_separate_cap_cases [where cap = cap]) apply (simp split del: if_split) apply (rule bisim_throwError, simp) apply (simp split del: if_split) apply (rule bisim_reflE) apply (fastforce intro!: bisim_throwError bisim_returnOk simp: AllowRecv_def AllowSend_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim ((=) \<oplus> (=)) (\<lambda>_. True) (K (separate_cap cap)) (Decode_SA.decode_invocation a b c d cap f) (Decode_A.decode_invocation a b c d cap f) proof (prove)
goal (1 subgoal):
 1. bisim ((=) \<oplus> (=)) (\<lambda>_. True) (K (separate_cap cap)) (case cap of NotificationCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0 | _ \<Rightarrow> throwError $ InvalidCapability 0) (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) proof (prove)
goal (3 subgoals):
 1. bisim ((=) \<oplus> (=)) ?Q ?Q' (case cap of NotificationCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0 | _ \<Rightarrow> throwError $ InvalidCapability 0) (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)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. K (separate_cap cap) s \<Longrightarrow> ?Q' s proof (prove)
goal (4 subgoals):
 1. cap = NullCap \<Longrightarrow> bisim ((=) \<oplus> (=)) ?Pn4 ?Pn'4 (case cap of NotificationCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0 | _ \<Rightarrow> throwError $ InvalidCapability 0) (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)
 2. \<And>ptr badge rights. cap = NotificationCap ptr badge rights \<Longrightarrow> bisim ((=) \<oplus> (=)) (?Pa4 ptr badge rights) (?Pa'4 ptr badge rights) (case cap of NotificationCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0 | _ \<Rightarrow> throwError $ InvalidCapability 0) (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)
 3. \<And>s. True \<Longrightarrow> (cap = NullCap \<longrightarrow> ?Pn4 s) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> ?Pa4 ptr badge rights s)
 4. \<And>s. K (separate_cap cap) s \<Longrightarrow> ((\<lambda>s. (cap = NullCap \<longrightarrow> ?Pn'4 s) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> ?Pa'4 ptr badge rights s)) and K (separate_cap cap)) s proof (prove)
goal (4 subgoals):
 1. cap = NullCap \<Longrightarrow> bisim ((=) \<oplus> (=)) ?Pn4 ?Pn'4 (throwError (InvalidCapability 0)) (throwError (InvalidCapability 0))
 2. \<And>ptr badge rights. cap = NotificationCap ptr badge rights \<Longrightarrow> bisim ((=) \<oplus> (=)) (?Pa4 ptr badge rights) (?Pa'4 ptr badge rights) (case cap of NotificationCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0 | _ \<Rightarrow> throwError $ InvalidCapability 0) (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)
 3. \<And>s. True \<Longrightarrow> (cap = NullCap \<longrightarrow> ?Pn4 s) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> ?Pa4 ptr badge rights s)
 4. \<And>s. K (separate_cap cap) s \<Longrightarrow> ((\<lambda>s. (cap = NullCap \<longrightarrow> ?Pn'4 s) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> ?Pa'4 ptr badge rights s)) and K (separate_cap cap)) s proof (prove)
goal (3 subgoals):
 1. \<And>ptr badge rights. cap = NotificationCap ptr badge rights \<Longrightarrow> bisim ((=) \<oplus> (=)) (?Pa4 ptr badge rights) (?Pa'4 ptr badge rights) (case cap of NotificationCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0 | _ \<Rightarrow> throwError $ InvalidCapability 0) (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)
 2. \<And>s. True \<Longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> ?Pa4 ptr badge rights s)
 3. \<And>s. K (separate_cap cap) s \<Longrightarrow> ((\<lambda>s. (cap = NullCap \<longrightarrow> True) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> ?Pa'4 ptr badge rights s)) and K (separate_cap cap)) s proof (prove)
goal (3 subgoals):
 1. \<And>ptr badge rights. cap = NotificationCap ptr badge rights \<Longrightarrow> bisim ((=) \<oplus> (=)) (?Pa4 ptr badge rights) (?Pa'4 ptr badge rights) (if AllowSend \<in> rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0) (if AllowSend \<in> rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0)
 2. \<And>s. True \<Longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> ?Pa4 ptr badge rights s)
 3. \<And>s. K (separate_cap cap) s \<Longrightarrow> ((\<lambda>s. (cap = NullCap \<longrightarrow> True) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> ?Pa'4 ptr badge rights s)) and K (separate_cap cap)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> (cap = NullCap \<longrightarrow> True) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> True)
 2. \<And>s. K (separate_cap cap) s \<Longrightarrow> ((\<lambda>s. (cap = NullCap \<longrightarrow> True) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> True)) and K (separate_cap cap)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. K (separate_cap cap) s \<Longrightarrow> ((\<lambda>s. (cap = NullCap \<longrightarrow> True) \<and> (\<forall>ptr badge rights. cap = NotificationCap ptr badge rights \<longrightarrow> True)) and K (separate_cap cap)) s proof (prove)
goal:
No subgoals!