theory ArchVSpaceEntries_AI

lemma decode_invocation_valid_pdpt[wp]:
  "\<lbrace>invs and valid_cap cap and valid_pdpt_objs\<rbrace>
     decode_invocation label args cap_index slot cap excaps
   \<lbrace>invocation_duplicates_valid\<rbrace>,-" apply (simp add: decode_invocation_def split del: if_split) apply (rule hoare_pre) apply (wp | wpc
            | simp only: invocation_duplicates_valid_def o_def uncurry_def split_def
                         Invocations_A.invocation.simps)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_cap cap and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> decode_invocation label args cap_index slot cap excaps \<lbrace>invocation_duplicates_valid\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_cap cap and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> case cap of UntypedCap dev ptr sz fi \<Rightarrow> liftME InvokeUntyped $ decode_untyped_invocation 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 label args cap (map fst excaps) | ThreadCap ptr \<Rightarrow> liftME InvokeTCB $ decode_tcb_invocation label args cap slot excaps | DomainCap \<Rightarrow> liftME (\<lambda>(x, y). InvokeDomain x y) $ decode_domain_invocation label args excaps | IRQControlCap \<Rightarrow> liftME InvokeIRQControl $ decode_irq_control_invocation label args slot (map fst excaps) | IRQHandlerCap irq \<Rightarrow> liftME InvokeIRQHandler $ decode_irq_handler_invocation label irq excaps | ArchObjectCap arch_cap \<Rightarrow> liftME InvokeArchObject $ arch_decode_invocation label args cap_index slot arch_cap excaps | _ \<Rightarrow> throwError $ InvalidCapability 0 \<lbrace>invocation_duplicates_valid\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case cap of UntypedCap dev ptr sz fi \<Rightarrow> liftME InvokeUntyped $ decode_untyped_invocation 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 label args cap (map fst excaps) | ThreadCap ptr \<Rightarrow> liftME InvokeTCB $ decode_tcb_invocation label args cap slot excaps | DomainCap \<Rightarrow> liftME (\<lambda>(x, y). InvokeDomain x y) $ decode_domain_invocation label args excaps | IRQControlCap \<Rightarrow> liftME InvokeIRQControl $ decode_irq_control_invocation label args slot (map fst excaps) | IRQHandlerCap irq \<Rightarrow> liftME InvokeIRQHandler $ decode_irq_handler_invocation label irq excaps | ArchObjectCap arch_cap \<Rightarrow> liftME InvokeArchObject $ arch_decode_invocation label args cap_index slot arch_cap excaps | _ \<Rightarrow> throwError $ InvalidCapability 0 \<lbrace>invocation_duplicates_valid\<rbrace>, -
 2. \<And>s. (invs and valid_cap cap and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and valid_cap cap and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) 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> True) \<and> (AllowSend \<notin> xb \<longrightarrow> True)) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> (AllowSend \<in> xb \<longrightarrow> 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> 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 valid_cap (ArchObjectCap x) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)) s) proof (prove)
goal:
No subgoals!