theory Tcb_DR

lemma decode_tcb_cap_label_not_match:
  "\<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> transform_intent (invocation_type label') args'; cap' = Structures_A.ThreadCap t\<rbrakk>
    \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_tcb_invocation label' args' cap' slot' excaps' \<lbrace>\<lambda>r. \<bottom>\<rbrace>,\<lbrace>\<lambda>e. (=) s\<rbrace>" apply (simp add:Decode_A.decode_tcb_invocation_def) apply (case_tac "gen_invocation_type label'") apply (simp_all add:transform_intent_def flip: gen_invocation_type_eq) apply wp apply (simp_all add: whenE_def transform_intent_tcb_defs
                  split: option.splits) apply (simp_all split:List.list.split list.split_asm option.splits add: gen_invocation_type_eq) apply (simp add: decode_read_registers_def decode_write_registers_def decode_set_ipc_buffer_def
                       decode_copy_registers_def decode_set_space_def decode_tcb_configure_def
                       decode_set_priority_def decode_set_mcpriority_def decode_set_sched_params_def
            | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> transform_intent (invocation_type label') args'; cap' = ThreadCap t\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_tcb_invocation label' args' cap' slot' excaps' \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> transform_intent (invocation_type label') args'; cap' = ThreadCap t\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (30 subgoals):
 1. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> transform_intent (invocation_type label') args'; cap' = ThreadCap t; gen_invocation_type label' = InvalidInvocation\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> transform_intent (invocation_type label') args'; cap' = ThreadCap t; gen_invocation_type label' = UntypedRetype\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 3. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> transform_intent (invocation_type label') args'; cap' = ThreadCap t; gen_invocation_type label' = TCBReadRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 4. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> transform_intent (invocation_type label') args'; cap' = ThreadCap t; gen_invocation_type label' = TCBWriteRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 5. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> transform_intent (invocation_type label') args'; cap' = ThreadCap t; gen_invocation_type label' = TCBCopyRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 6. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> transform_intent (invocation_type label') args'; cap' = ThreadCap t; gen_invocation_type label' = TCBConfigure\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 7. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> transform_intent (invocation_type label') args'; cap' = ThreadCap t; gen_invocation_type label' = TCBSetPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 8. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> transform_intent (invocation_type label') args'; cap' = ThreadCap t; gen_invocation_type label' = TCBSetMCPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 9. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> transform_intent (invocation_type label') args'; cap' = ThreadCap t; gen_invocation_type label' = TCBSetSchedParams\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 10. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> transform_intent (invocation_type label') args'; cap' = ThreadCap t; gen_invocation_type label' = TCBSetIPCBuffer\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
A total of 30 subgoals... proof (prove)
goal (25 subgoals):
 1. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> (case invocation_type label' of GenInvocationLabel InvalidInvocation \<Rightarrow> None | GenInvocationLabel UntypedRetype \<Rightarrow> map_option UntypedIntent (transform_intent_untyped_retype args') | GenInvocationLabel TCBReadRegisters \<Rightarrow> map_option TcbIntent (transform_intent_tcb_read_registers args') | GenInvocationLabel TCBWriteRegisters \<Rightarrow> map_option TcbIntent (transform_intent_tcb_write_registers args') | GenInvocationLabel TCBCopyRegisters \<Rightarrow> map_option TcbIntent (transform_intent_tcb_copy_registers args') | GenInvocationLabel TCBConfigure \<Rightarrow> map_option TcbIntent (transform_intent_tcb_configure args') | GenInvocationLabel TCBSetPriority \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_priority args') | GenInvocationLabel TCBSetMCPriority \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_mcpriority args') | GenInvocationLabel TCBSetSchedParams \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_sched_params args') | GenInvocationLabel TCBSetIPCBuffer \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_ipc_buffer args') | GenInvocationLabel TCBSetSpace \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_space args') | GenInvocationLabel TCBSuspend \<Rightarrow> Some (TcbIntent TcbSuspendIntent) | GenInvocationLabel TCBResume \<Rightarrow> Some (TcbIntent TcbResumeIntent) | GenInvocationLabel TCBBindNotification \<Rightarrow> Some (TcbIntent TcbBindNTFNIntent) | GenInvocationLabel TCBUnbindNotification \<Rightarrow> Some (TcbIntent TcbUnbindNTFNIntent) | GenInvocationLabel TCBSetTLSBase \<Rightarrow> Some (TcbIntent TcbSetTLSBaseIntent) | GenInvocationLabel CNodeRevoke \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeRevokeIntent args') | GenInvocationLabel CNodeDelete \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeDeleteIntent args') | GenInvocationLabel CNodeCancelBadgedSends \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeCancelBadgedSendsIntent args') | GenInvocationLabel CNodeCopy \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_copy args') | GenInvocationLabel CNodeMint \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_mint args') | GenInvocationLabel CNodeMove \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_move args') | GenInvocationLabel CNodeMutate \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_mutate args') | GenInvocationLabel CNodeRotate \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_rotate args') | GenInvocationLabel CNodeSaveCaller \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeSaveCallerIntent args') | GenInvocationLabel IRQIssueIRQHandler \<Rightarrow> map_option IrqControlIntent (transform_intent_issue_irq_handler args') | GenInvocationLabel IRQAckIRQ \<Rightarrow> Some (IrqHandlerIntent IrqHandlerAckIntent) | GenInvocationLabel IRQSetIRQHandler \<Rightarrow> Some (IrqHandlerIntent IrqHandlerSetEndpointIntent) | GenInvocationLabel IRQClearIRQHandler \<Rightarrow> Some (IrqHandlerIntent IrqHandlerClearIntent) | GenInvocationLabel DomainSetSet \<Rightarrow> map_option DomainIntent (transform_intent_domain args') | ArchInvocationLabel ARMPageTableMap \<Rightarrow> map_option PageTableIntent (transform_intent_page_table_map args') | ArchInvocationLabel ARMPageTableUnmap \<Rightarrow> Some (PageTableIntent PageTableUnmapIntent) | ArchInvocationLabel ARMPageMap \<Rightarrow> map_option PageIntent (transform_intent_page_map args') | ArchInvocationLabel ARMPageUnmap \<Rightarrow> Some (PageIntent PageUnmapIntent) | ArchInvocationLabel ARMPageClean_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageInvalidate_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageCleanInvalidate_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageUnify_Instruction \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageGetAddress \<Rightarrow> Some (PageIntent PageGetAddressIntent) | ArchInvocationLabel ARMASIDControlMakePool \<Rightarrow> map_option AsidControlIntent (transform_cnode_index_and_depth AsidControlMakePoolIntent args') | ArchInvocationLabel ARMASIDPoolAssign \<Rightarrow> Some (AsidPoolIntent AsidPoolAssignIntent) | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> map_option IrqControlIntent (arch_transform_intent_issue_irq_handler args') | ArchInvocationLabel _ \<Rightarrow> Some (PageDirectoryIntent PageDirectoryFlushIntent)); cap' = ThreadCap t; gen_invocation_type label' = InvalidInvocation\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option UntypedIntent (transform_intent_untyped_retype args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel UntypedRetype\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 3. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (transform_intent_tcb_read_registers args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBReadRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 4. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (transform_intent_tcb_write_registers args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBWriteRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 5. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (transform_intent_tcb_copy_registers args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBCopyRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 6. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (transform_intent_tcb_configure args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBConfigure\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 7. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (transform_intent_tcb_set_priority args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBSetPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 8. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (transform_intent_tcb_set_mcpriority args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBSetMCPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 9. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (transform_intent_tcb_set_sched_params args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBSetSchedParams\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 10. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (transform_intent_tcb_set_ipc_buffer args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBSetIPCBuffer\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
A total of 25 subgoals... proof (prove)
goal (24 subgoals):
 1. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option UntypedIntent (transform_intent_untyped_retype args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel UntypedRetype\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (transform_intent_tcb_read_registers args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBReadRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 3. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (transform_intent_tcb_write_registers args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBWriteRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 4. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (transform_intent_tcb_copy_registers args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBCopyRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 5. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (transform_intent_tcb_configure args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBConfigure\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 6. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (transform_intent_tcb_set_priority args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBSetPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 7. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (transform_intent_tcb_set_mcpriority args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBSetMCPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 8. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (transform_intent_tcb_set_sched_params args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBSetSchedParams\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 9. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (transform_intent_tcb_set_ipc_buffer args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBSetIPCBuffer\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 10. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (transform_intent_tcb_set_space args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBSetSpace\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
A total of 24 subgoals... proof (prove)
goal (24 subgoals):
 1. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option UntypedIntent (transform_intent_untyped_retype args'); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel UntypedRetype\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (case args' of [] \<Rightarrow> None | [flags] \<Rightarrow> None | flags # n # x \<Rightarrow> Some (TcbReadRegistersIntent (flags !! 0) 0 n)); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBReadRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 3. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (case args' of [] \<Rightarrow> None | [flags] \<Rightarrow> None | flags # n # values \<Rightarrow> Some (TcbWriteRegistersIntent (flags !! 0) 0 n values)); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBWriteRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 4. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (case args' of [] \<Rightarrow> None | flags # x \<Rightarrow> Some (TcbCopyRegistersIntent (flags !! 0) (flags !! 1) (flags !! 2) (flags !! 3) 0)); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBCopyRegisters\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 5. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (case args' of [] \<Rightarrow> None | [fault_ep] \<Rightarrow> None | [fault_ep, croot_data] \<Rightarrow> None | [fault_ep, croot_data, vroot_data] \<Rightarrow> None | fault_ep # croot_data # vroot_data # buffer # x \<Rightarrow> Some (TcbConfigureIntent fault_ep croot_data vroot_data buffer)); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBConfigure\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 6. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (case args' of [] \<Rightarrow> None | prio # x \<Rightarrow> Some (TcbSetPriorityIntent (prio_from_arg prio))); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBSetPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 7. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (case args' of [] \<Rightarrow> None | mcp # x \<Rightarrow> Some (TcbSetMCPriorityIntent (prio_from_arg mcp))); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBSetMCPriority\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 8. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (case args' of [] \<Rightarrow> None | [mcp] \<Rightarrow> None | mcp # priority # x \<Rightarrow> Some (TcbSetSchedParamsIntent (prio_from_arg mcp) (prio_from_arg priority))); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBSetSchedParams\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 9. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (case args' of [] \<Rightarrow> None | buffer # x \<Rightarrow> Some (TcbSetIPCBufferIntent buffer)); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBSetIPCBuffer\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 10. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option TcbIntent (case args' of [] \<Rightarrow> None | [fault_ep] \<Rightarrow> None | [fault_ep, croot_data] \<Rightarrow> None | fault_ep # croot_data # vroot_data # x \<Rightarrow> Some (TcbSetSpaceIntent fault_ep croot_data vroot_data)); cap' = ThreadCap t; invocation_type label' = GenInvocationLabel TCBSetSpace\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case gen_invocation_type label' of TCBReadRegisters \<Rightarrow> decode_read_registers args' (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers args' (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers args' (ThreadCap t) $ map fst excaps' | TCBConfigure \<Rightarrow> decode_tcb_configure args' (ThreadCap t) slot' excaps' | TCBSetPriority \<Rightarrow> decode_set_priority args' (ThreadCap t) slot' excaps' | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args' (ThreadCap t) slot' excaps' | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args' (ThreadCap t) slot' excaps' | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args' (ThreadCap t) slot' excaps' | TCBSetSpace \<Rightarrow> decode_set_space args' (ThreadCap t) slot' excaps' | TCBSuspend \<Rightarrow> returnOk $ tcb_invocation.Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ tcb_invocation.Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) excaps' | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args' (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
A total of 24 subgoals... proof (prove)
goal (32 subgoals):
 1. \<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> map_option UntypedIntent (transform_intent_untyped_retype args'); cap' = ThreadCap t; gen_invocation_type label' = UntypedRetype\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>cap' = ThreadCap t; gen_invocation_type label' = TCBReadRegisters; args' = []\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_read_registers [] (ThreadCap t) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 3. \<And>x21 x22. \<lbrakk>cap' = ThreadCap t; gen_invocation_type label' = TCBReadRegisters; args' = [x21]; x22 = []\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_read_registers [x21] (ThreadCap t) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 4. \<lbrakk>cap' = ThreadCap t; gen_invocation_type label' = TCBWriteRegisters; args' = []\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_write_registers [] (ThreadCap t) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 5. \<And>x21 x22. \<lbrakk>cap' = ThreadCap t; gen_invocation_type label' = TCBWriteRegisters; args' = [x21]; x22 = []\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_write_registers [x21] (ThreadCap t) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 6. \<lbrakk>cap' = ThreadCap t; gen_invocation_type label' = TCBCopyRegisters; args' = []\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_copy_registers [] (ThreadCap t) (map fst excaps') \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 7. \<lbrakk>cap' = ThreadCap t; gen_invocation_type label' = TCBConfigure; args' = []\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_tcb_configure [] (ThreadCap t) slot' excaps' \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 8. \<And>x21 x22. \<lbrakk>cap' = ThreadCap t; gen_invocation_type label' = TCBConfigure; args' = [x21]; x22 = []\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_tcb_configure [x21] (ThreadCap t) slot' excaps' \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 9. \<And>x21 x22 x21a x22a. \<lbrakk>cap' = ThreadCap t; gen_invocation_type label' = TCBConfigure; args' = [x21, x21a]; x22 = [x21a]; x22a = []\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_tcb_configure [x21, x21a] (ThreadCap t) slot' excaps' \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 10. \<And>x21 x22 x21a x22a x21b x22b. \<lbrakk>cap' = ThreadCap t; gen_invocation_type label' = TCBConfigure; args' = [x21, x21a, x21b]; x22 = [x21a, x21b]; x22a = [x21b]; x22b = []\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_tcb_configure [x21, x21a, x21b] (ThreadCap t) slot' excaps' \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
A total of 32 subgoals... proof (prove)
goal:
No subgoals!