theory Syscall_R

lemma decode_inv_inv'[wp]:
  "\<lbrace>P\<rbrace> decodeInvocation label args cap_index slot cap excaps \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: decodeInvocation_def Let_def
              split del: if_split
              cong: if_cong) apply (rule hoare_pre) apply (wp decodeTCBInvocation_inv |
          simp only: o_def |
          clarsimp split: capability.split_asm simp: isCap_defs)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> global.decodeInvocation label args cap_index slot cap excaps \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> if isEndpointCap cap \<and> capEPCanSend cap then returnOk (Invocations_H.invocation.InvokeEndpoint (capEPPtr cap) (capEPBadge cap) (capEPCanGrant cap) (capEPCanGrantReply cap)) else if isNotificationCap cap \<and> capNtfnCanSend cap then returnOk (Invocations_H.invocation.InvokeNotification (capNtfnPtr cap) (capNtfnBadge cap)) else if isReplyCap cap \<and> \<not> capReplyMaster cap then returnOk (Invocations_H.invocation.InvokeReply (capTCBPtr cap) slot (capReplyCanGrant cap)) else if isThreadCap cap then liftME Invocations_H.invocation.InvokeTCB (decodeTCBInvocation label args cap slot excaps) else if cap = capability.DomainCap then liftME (uncurry Invocations_H.invocation.InvokeDomain) (decodeDomainInvocation label args excaps) else if isCNodeCap cap then liftME Invocations_H.invocation.InvokeCNode (decodeCNodeInvocation label args cap (map fst excaps)) else if isUntypedCap cap then liftME Invocations_H.invocation.InvokeUntyped (decodeUntypedInvocation label args slot cap (map fst excaps)) else if isIRQControlCap cap then liftME Invocations_H.invocation.InvokeIRQControl (global.decodeIRQControlInvocation label args slot (map fst excaps)) else if isIRQHandlerCap cap then liftME Invocations_H.invocation.InvokeIRQHandler (decodeIRQHandlerInvocation label (capIRQ cap) excaps) else if isArchObjectCap cap then liftME Invocations_H.invocation.InvokeArchObject (Arch.decodeInvocation label args cap_index slot (capCap cap) excaps) else throwError (Fault_H.syscall_error.InvalidCapability 0) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q22\<rbrace> if isEndpointCap cap \<and> capEPCanSend cap then returnOk (Invocations_H.invocation.InvokeEndpoint (capEPPtr cap) (capEPBadge cap) (capEPCanGrant cap) (capEPCanGrantReply cap)) else if isNotificationCap cap \<and> capNtfnCanSend cap then returnOk (Invocations_H.invocation.InvokeNotification (capNtfnPtr cap) (capNtfnBadge cap)) else if isReplyCap cap \<and> \<not> capReplyMaster cap then returnOk (Invocations_H.invocation.InvokeReply (capTCBPtr cap) slot (capReplyCanGrant cap)) else if isThreadCap cap then liftME Invocations_H.invocation.InvokeTCB (decodeTCBInvocation label args cap slot excaps) else if cap = capability.DomainCap then liftME (uncurry Invocations_H.invocation.InvokeDomain) (decodeDomainInvocation label args excaps) else if isCNodeCap cap then liftME Invocations_H.invocation.InvokeCNode (decodeCNodeInvocation label args cap (map fst excaps)) else if isUntypedCap cap then liftME Invocations_H.invocation.InvokeUntyped (decodeUntypedInvocation label args slot cap (map fst excaps)) else if isIRQControlCap cap then liftME Invocations_H.invocation.InvokeIRQControl (global.decodeIRQControlInvocation label args slot (map fst excaps)) else if isIRQHandlerCap cap then liftME Invocations_H.invocation.InvokeIRQHandler (decodeIRQHandlerInvocation label (capIRQ cap) excaps) else if isArchObjectCap cap then liftME Invocations_H.invocation.InvokeArchObject (Arch.decodeInvocation label args cap_index slot (capCap cap) excaps) else throwError (Fault_H.syscall_error.InvalidCapability 0) \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q22 s proof (prove)
goal:
No subgoals!