theory Invocation_DP

lemma decode_invocation_nonep:
  "\<lbrace>\<lambda>s. \<not> ep_related_cap cap \<rbrace>
   decode_invocation cap cap_ref extra_caps intent
   \<lbrace>\<lambda>rv s. nonep_invocation rv\<rbrace>, -" apply (simp add: decode_invocation_def) apply (wpsimp simp: o_def nonep_invocation_def simp_del: hoare_True_E_R) apply (auto simp: ep_related_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> ep_related_cap cap\<rbrace> decode_invocation cap cap_ref extra_caps intent \<lbrace>\<lambda>rv s. nonep_invocation rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> ep_related_cap cap\<rbrace> case cap of UntypedCap x xa xb \<Rightarrow> doE untyped_intent <- throw_opt undefined $ get_untyped_intent intent;
liftME InvokeUntyped $ decode_untyped_invocation cap cap_ref extra_caps untyped_intent
odE | EndpointCap o_id badge rights \<Rightarrow> if AllowWrite \<in> rights then returnOk $ InvokeEndpoint (SyncMessage badge (AllowGrant \<in> rights) (AllowGrantReply \<in> rights) o_id) else throw | NotificationCap o_id badge rights \<Rightarrow> if AllowWrite \<in> rights then returnOk $ InvokeNotification (Signal badge o_id) else throw | ReplyCap o_id rights \<Rightarrow> returnOk $ InvokeReply (ReplyMessage o_id cap_ref (AllowGrant \<in> rights)) | CNodeCap x xa xb xc \<Rightarrow> doE cnode_intent <- throw_opt undefined $ get_cnode_intent intent;
liftME InvokeCNode $ decode_cnode_invocation cap cap_ref extra_caps cnode_intent
odE | TcbCap x \<Rightarrow> doE tcb_intent <- throw_opt undefined $ get_tcb_intent intent;
liftME InvokeTcb $ decode_tcb_invocation cap cap_ref extra_caps tcb_intent
odE | DomainCap \<Rightarrow> doE domain_intent <- throw_opt undefined $ get_domain_intent intent;
liftME InvokeDomain $ decode_domain_invocation extra_caps domain_intent
odE | IrqControlCap \<Rightarrow> doE irq_control_intent <- throw_opt undefined $ get_irq_control_intent intent;
liftME InvokeIrqControl $ decode_irq_control_invocation cap cap_ref extra_caps irq_control_intent
odE | IrqHandlerCap x \<Rightarrow> doE irq_handler_intent <- throw_opt undefined $ get_irq_handler_intent intent;
liftME InvokeIrqHandler $ decode_irq_handler_invocation cap cap_ref extra_caps irq_handler_intent
odE | FrameCap x xa xb xc xd xe \<Rightarrow> doE page_intent <- throw_opt undefined $ get_page_intent intent;
liftME InvokePage $ decode_page_invocation cap cap_ref extra_caps page_intent
odE | PageTableCap x xa xb \<Rightarrow> doE page_table_intent <- throw_opt undefined $ get_page_table_intent intent;
liftME InvokePageTable $ decode_page_table_invocation cap cap_ref extra_caps page_table_intent
odE | PageDirectoryCap x xa xb \<Rightarrow> doE page_directory_intent <- throw_opt undefined $ get_page_directory_intent intent;
liftME InvokePageDirectory $ decode_page_directory_invocation cap cap_ref extra_caps page_directory_intent
odE | AsidControlCap \<Rightarrow> doE asid_control_intent <- throw_opt undefined $ get_asid_control_intent intent;
liftME InvokeAsidControl $ decode_asid_control_invocation cap cap_ref extra_caps asid_control_intent
odE | AsidPoolCap x xa \<Rightarrow> doE asid_pool_intent <- throw_opt undefined $ get_asid_pool_intent intent;
liftME InvokeAsidPool $ decode_asid_pool_invocation cap cap_ref extra_caps asid_pool_intent
odE | _ \<Rightarrow> throw \<lbrace>\<lambda>rv s. nonep_invocation rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<not> ep_related_cap cap \<Longrightarrow> (\<forall>x xa xb. cap = EndpointCap x xa xb \<longrightarrow> AllowWrite \<notin> xb) \<and> (\<forall>x xa xb. cap = NotificationCap x xa xb \<longrightarrow> AllowWrite \<notin> xb) \<and> (\<forall>x xa. cap \<noteq> ReplyCap x xa) proof (prove)
goal:
No subgoals!