theory Syscall_DR

lemma decode_invocation_cnodecap_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.CNodeCap a b c \<rbrakk> \<Longrightarrow>
    dcorres (dc \<oplus> cdl_invocation_relation) \<top>
        (invs and valid_cap invoked_cap' and (\<lambda>s. \<forall>e\<in>set excaps'. valid_cap (fst e) s) and valid_etcbs)
        (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 (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def) apply (case_tac "\<exists> ui. intent = CNodeIntent ui") apply (rotate_tac -1, erule exE) apply (rotate_tac -1, drule sym) apply (clarsimp simp: get_cnode_intent_def throw_opt_def split: cdl_intent.split) apply (rule dcorres_liftME_liftME) apply (rule decode_cnode_corres, auto simp: transform_cap_def)[1] apply (clarsimp simp: cdl_invocation_relation_def translate_invocation_def) apply (clarsimp simp: throw_opt_def get_cnode_intent_def split: cdl_intent.split) apply (rule absorb_imp,clarsimp)+ apply (rule dcorres_free_throw) apply (subst decode_cnode_label_not_match) apply simp+ 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.CNodeCap a b c\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and valid_cap invoked_cap' and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) (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 = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) (doE cnode_intent <- throw_opt undefined (get_cnode_intent intent);
liftME cdl_invocation.InvokeCNode (CNode_D.decode_cnode_invocation (cdl_cap.CNodeCap a (of_bl c) (length c) b) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') cnode_intent)
odE) (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; \<exists>ui. intent = CNodeIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) (doE cnode_intent <- throw_opt undefined (get_cnode_intent intent);
liftME cdl_invocation.InvokeCNode (CNode_D.decode_cnode_invocation (cdl_cap.CNodeCap a (of_bl c) (length c) b) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') cnode_intent)
odE) (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps'))
 2. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; \<nexists>ui. intent = CNodeIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) (doE cnode_intent <- throw_opt undefined (get_cnode_intent intent);
liftME cdl_invocation.InvokeCNode (CNode_D.decode_cnode_invocation (cdl_cap.CNodeCap a (of_bl c) (length c) b) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') cnode_intent)
odE) (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps')) proof (prove)
goal (2 subgoals):
 1. \<And>ui. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; intent = CNodeIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) (doE cnode_intent <- throw_opt undefined (get_cnode_intent intent);
liftME cdl_invocation.InvokeCNode (CNode_D.decode_cnode_invocation (cdl_cap.CNodeCap a (of_bl c) (length c) b) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') cnode_intent)
odE) (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps'))
 2. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; \<nexists>ui. intent = CNodeIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) (doE cnode_intent <- throw_opt undefined (get_cnode_intent intent);
liftME cdl_invocation.InvokeCNode (CNode_D.decode_cnode_invocation (cdl_cap.CNodeCap a (of_bl c) (length c) b) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') cnode_intent)
odE) (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps')) proof (prove)
goal (2 subgoals):
 1. \<And>ui. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; CNodeIntent ui = intent\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) (doE cnode_intent <- throw_opt undefined (get_cnode_intent intent);
liftME cdl_invocation.InvokeCNode (CNode_D.decode_cnode_invocation (cdl_cap.CNodeCap a (of_bl c) (length c) b) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') cnode_intent)
odE) (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps'))
 2. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; \<nexists>ui. intent = CNodeIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) (doE cnode_intent <- throw_opt undefined (get_cnode_intent intent);
liftME cdl_invocation.InvokeCNode (CNode_D.decode_cnode_invocation (cdl_cap.CNodeCap a (of_bl c) (length c) b) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') cnode_intent)
odE) (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps')) proof (prove)
goal (2 subgoals):
 1. \<And>ui. \<lbrakk>Some (CNodeIntent ui) = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; intent = CNodeIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode) \<circ> cdl_invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) (CNode_D.decode_cnode_invocation (cdl_cap.CNodeCap a (of_bl c) (length c) b) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') ui) (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps'))
 2. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; \<nexists>ui. intent = CNodeIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) (doE cnode_intent <- throw_opt undefined (get_cnode_intent intent);
liftME cdl_invocation.InvokeCNode (CNode_D.decode_cnode_invocation (cdl_cap.CNodeCap a (of_bl c) (length c) b) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') cnode_intent)
odE) (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps')) proof (prove)
goal (3 subgoals):
 1. \<And>ui. \<lbrakk>Some (CNodeIntent ui) = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; intent = CNodeIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ?rvrel15 ui) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) (CNode_D.decode_cnode_invocation (cdl_cap.CNodeCap a (of_bl c) (length c) b) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') ui) (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps'))
 2. \<And>ui r r'. \<lbrakk>Some (CNodeIntent ui) = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; intent = CNodeIntent ui; ?rvrel15 ui r r'\<rbrakk> \<Longrightarrow> cdl_invocation_relation (cdl_invocation.InvokeCNode r) (invocation.InvokeCNode r')
 3. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; \<nexists>ui. intent = CNodeIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) (doE cnode_intent <- throw_opt undefined (get_cnode_intent intent);
liftME cdl_invocation.InvokeCNode (CNode_D.decode_cnode_invocation (cdl_cap.CNodeCap a (of_bl c) (length c) b) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') cnode_intent)
odE) (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps')) proof (prove)
goal (2 subgoals):
 1. \<And>ui r r'. \<lbrakk>Some (CNodeIntent ui) = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; intent = CNodeIntent ui; r = translate_cnode_invocation r'\<rbrakk> \<Longrightarrow> cdl_invocation_relation (cdl_invocation.InvokeCNode r) (invocation.InvokeCNode r')
 2. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; \<nexists>ui. intent = CNodeIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) (doE cnode_intent <- throw_opt undefined (get_cnode_intent intent);
liftME cdl_invocation.InvokeCNode (CNode_D.decode_cnode_invocation (cdl_cap.CNodeCap a (of_bl c) (length c) b) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') cnode_intent)
odE) (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst 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 = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; \<nexists>ui. intent = CNodeIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) (doE cnode_intent <- throw_opt undefined (get_cnode_intent intent);
liftME cdl_invocation.InvokeCNode (CNode_D.decode_cnode_invocation (cdl_cap.CNodeCap a (of_bl c) (length c) b) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') cnode_intent)
odE) (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst 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 = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; \<forall>ui. intent \<noteq> CNodeIntent ui\<rbrakk> \<Longrightarrow> ((\<exists>x2. intent = TcbIntent x2) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) throw (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps'))) \<and> ((\<exists>x3. intent = UntypedIntent x3) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) throw (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps'))) \<and> ((\<exists>x4. intent = IrqHandlerIntent x4) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) throw (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps'))) \<and> ((\<exists>x5. intent = IrqControlIntent x5) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) throw (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps'))) \<and> ((\<exists>x6. intent = PageTableIntent x6) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) throw (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps'))) \<and> ((\<exists>x7. intent = PageIntent x7) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) throw (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps'))) \<and> ((\<exists>x8. intent = PageDirectoryIntent x8) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) throw (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps'))) \<and> ((\<exists>x9. intent = AsidControlIntent x9) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) throw (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps'))) \<and> ((\<exists>x10. intent = AsidPoolIntent x10) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) throw (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps'))) \<and> ((\<exists>x11. intent = NotificationIntent x11) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) throw (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps'))) \<and> ((\<exists>x12. intent = EndpointIntent x12) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) throw (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps'))) \<and> ((\<exists>x13. intent = DomainIntent x13) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) throw (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst 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 = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; \<forall>ui. intent \<noteq> CNodeIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeCNode)) (\<lambda>_. True) (invs and valid_cap (cap.CNodeCap a b c) and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_etcbs) throw (Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps')) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; \<forall>ui. intent \<noteq> CNodeIntent ui\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_cnode_invocation label' args' (cap.CNodeCap a b c) (map fst excaps') \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; \<forall>ui. intent \<noteq> CNodeIntent ui\<rbrakk> \<Longrightarrow> Some (?intent62 s) = transform_intent (invocation_type label') args'
 2. \<And>s. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; \<forall>ui. intent \<noteq> CNodeIntent ui\<rbrakk> \<Longrightarrow> \<forall>ui. ?intent62 s \<noteq> CNodeIntent ui
 3. \<And>s. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.CNodeCap a (of_bl c) (length c) b; excaps = transform_cap_list excaps'; invoked_cap' = cap.CNodeCap a b c; \<forall>ui. intent \<noteq> CNodeIntent ui\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals!