theory Syscall_DR

lemma decode_invocation_error_branch:
  "\<lbrakk>transform_intent (invocation_type label) args = None; \<not> ep_related_cap (transform_cap cap)\<rbrakk>
    \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>,\<lbrace>\<lambda>x. (=) s\<rbrace>" apply (case_tac cap) apply (simp_all add:ep_related_cap_def transform_cap_def split:if_split_asm) apply (clarsimp simp:Decode_A.decode_invocation_def,wp) apply (rule transform_intent_untyped_cap_None,fastforce+) apply (clarsimp simp:Decode_A.decode_invocation_def,wp) apply (rule transform_intent_cnode_cap_None,fastforce+) apply (rule transform_intent_thread_cap_None,fastforce+) apply (rule transform_intent_domain_cap_None,fastforce+) apply (rule transform_intent_irq_control_None,fastforce+) apply (rule transform_intent_irq_handler_None,fastforce+) apply (rule transform_intent_zombie_cap_None,fastforce+) apply (rule transform_intent_arch_cap_None,fastforce+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> ep_related_cap (transform_cap cap)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> ep_related_cap (transform_cap cap); cap = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x21 x22 x23 x24. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> ep_related_cap (transform_cap cap); cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>x31 x32 x33. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> ep_related_cap (transform_cap cap); cap = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<And>x41 x42 x43. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> ep_related_cap (transform_cap cap); cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<And>x51 x52 x53. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> ep_related_cap (transform_cap cap); cap = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<And>x61 x62 x63. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> ep_related_cap (transform_cap cap); cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 7. \<And>x7. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> ep_related_cap (transform_cap cap); cap = ThreadCap x7\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 8. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> ep_related_cap (transform_cap cap); cap = cap.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 9. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> ep_related_cap (transform_cap cap); cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 10. \<And>x10. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> ep_related_cap (transform_cap cap); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
A total of 12 subgoals... proof (prove)
goal (10 subgoals):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap.NullCap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x21 x22 x23 x24. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (cap.UntypedCap x21 x22 x23 x24) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>x51 x52 x53. \<lbrakk>cap = cap.ReplyCap x51 True x53; transform_intent (invocation_type label) args = None; x52\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (cap.ReplyCap x51 True x53) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<And>x61 x62 x63. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (cap.CNodeCap x61 x62 x63) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<And>x7. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (ThreadCap x7) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap.DomainCap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 7. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot IRQControlCap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 8. \<And>x10. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (IRQHandlerCap x10) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 9. \<And>x111 x112 x113. \<lbrakk>transform_intent (invocation_type label) args = None; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (Zombie x111 x112 x113) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 10. \<And>x12. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> (case case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap o_id badge rights \<Rightarrow> True | cdl_cap.NotificationCap o_id badge rights \<Rightarrow> True | cdl_cap.ReplyCap o_id rights \<Rightarrow> True | _ \<Rightarrow> False); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (ArchObjectCap x12) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (cap.UntypedCap x21 x22 x23 x24) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x51 x52 x53. \<lbrakk>cap = cap.ReplyCap x51 True x53; transform_intent (invocation_type label) args = None; x52\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (cap.ReplyCap x51 True x53) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>x61 x62 x63. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (cap.CNodeCap x61 x62 x63) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<And>x7. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (ThreadCap x7) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap.DomainCap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot IRQControlCap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 7. \<And>x10. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (IRQHandlerCap x10) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 8. \<And>x111 x112 x113. \<lbrakk>transform_intent (invocation_type label) args = None; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (Zombie x111 x112 x113) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 9. \<And>x12. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> (case case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap o_id badge rights \<Rightarrow> True | cdl_cap.NotificationCap o_id badge rights \<Rightarrow> True | cdl_cap.ReplyCap o_id rights \<Rightarrow> True | _ \<Rightarrow> False); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (ArchObjectCap x12) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x51 x52 x53. \<lbrakk>cap = cap.ReplyCap x51 True x53; transform_intent (invocation_type label) args = None; x52\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (cap.ReplyCap x51 True x53) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x61 x62 x63. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (cap.CNodeCap x61 x62 x63) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>x7. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (ThreadCap x7) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap.DomainCap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot IRQControlCap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<And>x10. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (IRQHandlerCap x10) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 7. \<And>x111 x112 x113. \<lbrakk>transform_intent (invocation_type label) args = None; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (Zombie x111 x112 x113) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 8. \<And>x12. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> (case case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap o_id badge rights \<Rightarrow> True | cdl_cap.NotificationCap o_id badge rights \<Rightarrow> True | cdl_cap.ReplyCap o_id rights \<Rightarrow> True | _ \<Rightarrow> False); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (ArchObjectCap x12) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (cap.CNodeCap x61 x62 x63) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x7. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (ThreadCap x7) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap.DomainCap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot IRQControlCap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<And>x10. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (IRQHandlerCap x10) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<And>x111 x112 x113. \<lbrakk>transform_intent (invocation_type label) args = None; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (Zombie x111 x112 x113) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 7. \<And>x12. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> (case case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap o_id badge rights \<Rightarrow> True | cdl_cap.NotificationCap o_id badge rights \<Rightarrow> True | cdl_cap.ReplyCap o_id rights \<Rightarrow> True | _ \<Rightarrow> False); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (ArchObjectCap x12) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x7. \<lbrakk>transform_intent (invocation_type label) args = None; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (ThreadCap x7) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap.DomainCap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot IRQControlCap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<And>x10. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (IRQHandlerCap x10) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<And>x111 x112 x113. \<lbrakk>transform_intent (invocation_type label) args = None; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (Zombie x111 x112 x113) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 6. \<And>x12. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> (case case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap o_id badge rights \<Rightarrow> True | cdl_cap.NotificationCap o_id badge rights \<Rightarrow> True | cdl_cap.ReplyCap o_id rights \<Rightarrow> True | _ \<Rightarrow> False); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (ArchObjectCap x12) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap.DomainCap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot IRQControlCap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>x10. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (IRQHandlerCap x10) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<And>x111 x112 x113. \<lbrakk>transform_intent (invocation_type label) args = None; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (Zombie x111 x112 x113) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 5. \<And>x12. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> (case case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap o_id badge rights \<Rightarrow> True | cdl_cap.NotificationCap o_id badge rights \<Rightarrow> True | cdl_cap.ReplyCap o_id rights \<Rightarrow> True | _ \<Rightarrow> False); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (ArchObjectCap x12) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot IRQControlCap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x10. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (IRQHandlerCap x10) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>x111 x112 x113. \<lbrakk>transform_intent (invocation_type label) args = None; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (Zombie x111 x112 x113) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 4. \<And>x12. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> (case case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap o_id badge rights \<Rightarrow> True | cdl_cap.NotificationCap o_id badge rights \<Rightarrow> True | cdl_cap.ReplyCap o_id rights \<Rightarrow> True | _ \<Rightarrow> False); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (ArchObjectCap x12) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x10. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (IRQHandlerCap x10) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x111 x112 x113. \<lbrakk>transform_intent (invocation_type label) args = None; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (Zombie x111 x112 x113) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>x12. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> (case case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap o_id badge rights \<Rightarrow> True | cdl_cap.NotificationCap o_id badge rights \<Rightarrow> True | cdl_cap.ReplyCap o_id rights \<Rightarrow> True | _ \<Rightarrow> False); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (ArchObjectCap x12) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x111 x112 x113. \<lbrakk>transform_intent (invocation_type label) args = None; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (Zombie x111 x112 x113) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x12. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> (case case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap o_id badge rights \<Rightarrow> True | cdl_cap.NotificationCap o_id badge rights \<Rightarrow> True | cdl_cap.ReplyCap o_id rights \<Rightarrow> True | _ \<Rightarrow> False); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (ArchObjectCap x12) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>transform_intent (invocation_type label) args = None; \<not> (case case x12 of ASIDPoolCap ptr asid \<Rightarrow> AsidPoolCap ptr (fst $ transform_asid asid) | ASIDControlCap \<Rightarrow> AsidControlCap | PageCap dev ptr cap_rights_ sz mp \<Rightarrow> FrameCap dev ptr cap_rights_ (pageBitsForSize sz) Real (transform_mapping mp) | arch_cap.PageTableCap ptr mp \<Rightarrow> cdl_cap.PageTableCap ptr Real (transform_mapping mp) | arch_cap.PageDirectoryCap ptr mp \<Rightarrow> cdl_cap.PageDirectoryCap ptr Real (map_option transform_asid mp) of cdl_cap.EndpointCap o_id badge rights \<Rightarrow> True | cdl_cap.NotificationCap o_id badge rights \<Rightarrow> True | cdl_cap.ReplyCap o_id rights \<Rightarrow> True | _ \<Rightarrow> False); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot (ArchObjectCap x12) excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal:
No subgoals!