theory Syscall_DR

lemma decode_invocation_nullcap_corres:
  "\<lbrakk> Some intent = transform_intent (invocation_type label) args';
     invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
     invoked_cap = transform_cap invoked_cap';
     excaps = transform_cap_list excaps';
     invoked_cap' = cap.NullCap \<rbrakk> \<Longrightarrow>
    dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top>
        (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
        (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')" apply (unfold  Decode_A.decode_invocation_def Decode_D.decode_invocation_def) apply (clarsimp simp: transform_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = transform_cap invoked_cap'; excaps = transform_cap_list excaps'; invoked_cap' = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = transform_cap invoked_cap'; excaps = transform_cap_list excaps'; invoked_cap' = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (case invoked_cap of cdl_cap.UntypedCap x xa xb \<Rightarrow> doE untyped_intent <- throw_opt undefined $ get_untyped_intent intent;
liftME cdl_invocation.InvokeUntyped $ Untyped_D.decode_untyped_invocation invoked_cap invoked_cap_ref excaps untyped_intent
odE | cdl_cap.EndpointCap o_id badge rights \<Rightarrow> if AllowWrite \<in> rights then returnOk $ cdl_invocation.InvokeEndpoint (SyncMessage badge (AllowGrant \<in> rights) (AllowGrantReply \<in> rights) o_id) else throw | cdl_cap.NotificationCap o_id badge rights \<Rightarrow> if AllowWrite \<in> rights then returnOk $ cdl_invocation.InvokeNotification (Signal badge o_id) else throw | cdl_cap.ReplyCap o_id rights \<Rightarrow> returnOk $ cdl_invocation.InvokeReply (ReplyMessage o_id invoked_cap_ref (AllowGrant \<in> rights)) | cdl_cap.CNodeCap x xa xb xc \<Rightarrow> doE cnode_intent <- throw_opt undefined $ get_cnode_intent intent;
liftME cdl_invocation.InvokeCNode $ CNode_D.decode_cnode_invocation invoked_cap invoked_cap_ref excaps cnode_intent
odE | TcbCap x \<Rightarrow> doE tcb_intent <- throw_opt undefined $ get_tcb_intent intent;
liftME InvokeTcb $ Tcb_D.decode_tcb_invocation invoked_cap invoked_cap_ref excaps tcb_intent
odE | cdl_cap.DomainCap \<Rightarrow> doE domain_intent <- throw_opt undefined $ get_domain_intent intent;
liftME cdl_invocation.InvokeDomain $ Tcb_D.decode_domain_invocation excaps domain_intent
odE | IrqControlCap \<Rightarrow> doE irq_control_intent <- throw_opt undefined $ get_irq_control_intent intent;
liftME InvokeIrqControl $ Interrupt_D.decode_irq_control_invocation invoked_cap invoked_cap_ref excaps irq_control_intent
odE | IrqHandlerCap x \<Rightarrow> doE irq_handler_intent <- throw_opt undefined $ get_irq_handler_intent intent;
liftME InvokeIrqHandler $ Interrupt_D.decode_irq_handler_invocation invoked_cap invoked_cap_ref excaps irq_handler_intent
odE | FrameCap x xa xb xc xd xe \<Rightarrow> doE page_intent <- throw_opt undefined $ get_page_intent intent;
liftME cdl_invocation.InvokePage $ decode_page_invocation invoked_cap invoked_cap_ref excaps page_intent
odE | cdl_cap.PageTableCap x xa xb \<Rightarrow> doE page_table_intent <- throw_opt undefined $ get_page_table_intent intent;
liftME cdl_invocation.InvokePageTable $ decode_page_table_invocation invoked_cap invoked_cap_ref excaps page_table_intent
odE | cdl_cap.PageDirectoryCap x xa xb \<Rightarrow> doE page_directory_intent <- throw_opt undefined $ get_page_directory_intent intent;
liftME cdl_invocation.InvokePageDirectory $ decode_page_directory_invocation invoked_cap invoked_cap_ref excaps page_directory_intent
odE | AsidControlCap \<Rightarrow> doE asid_control_intent <- throw_opt undefined $ get_asid_control_intent intent;
liftME InvokeAsidControl $ decode_asid_control_invocation invoked_cap invoked_cap_ref excaps 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 invoked_cap invoked_cap_ref excaps asid_pool_intent
odE | _ \<Rightarrow> throw) (case invoked_cap' of cap.UntypedCap dev ptr sz fi \<Rightarrow> liftME invocation.InvokeUntyped $ Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' invoked_cap' (map fst excaps') | cap.EndpointCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ invocation.InvokeEndpoint ptr badge (AllowGrant \<in> rights) (AllowGrantReply \<in> rights) else throwError $ InvalidCapability 0 | cap.NotificationCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ invocation.InvokeNotification ptr badge else throwError $ InvalidCapability 0 | cap.ReplyCap thread True rights \<Rightarrow> throwError $ InvalidCapability 0 | cap.ReplyCap thread False rights \<Rightarrow> returnOk $ invocation.InvokeReply thread invoked_cap_ref' (AllowGrant \<in> rights) | cap.CNodeCap ptr bits x \<Rightarrow> liftME invocation.InvokeCNode $ Decode_A.decode_cnode_invocation label' args' invoked_cap' (map fst excaps') | ThreadCap ptr \<Rightarrow> liftME InvokeTCB $ Decode_A.decode_tcb_invocation label' args' invoked_cap' invoked_cap_ref' excaps' | cap.DomainCap \<Rightarrow> liftME (\<lambda>(x, y). invocation.InvokeDomain x y) $ Decode_A.decode_domain_invocation label' args' excaps' | IRQControlCap \<Rightarrow> liftME InvokeIRQControl $ Decode_A.decode_irq_control_invocation label' args' invoked_cap_ref' (map fst excaps') | IRQHandlerCap irq \<Rightarrow> liftME InvokeIRQHandler $ Decode_A.decode_irq_handler_invocation label' irq excaps' | ArchObjectCap arch_cap \<Rightarrow> liftME InvokeArchObject $ arch_decode_invocation label' args' cap_index' invoked_cap_ref' arch_cap excaps' | _ \<Rightarrow> throwError $ InvalidCapability 0) proof (prove)
goal:
No subgoals!