theory Tcb_AI

lemma (in Tcb_AI) decode_tcb_inv_inv:
  "\<lbrace>P::'state_ext state \<Rightarrow> bool\<rbrace>
     decode_tcb_invocation label args (cap.ThreadCap t) slot extras
   \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: decode_tcb_invocation_def Let_def decode_set_tls_base_def
             cong: if_cong
        split del: if_split) apply (rule hoare_pre) apply (wpc
        | wp decode_readreg_inv decode_writereg_inv
             decode_copyreg_inv decode_tcb_conf_inv
             decode_set_tls_base_inv)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_tcb_invocation label args (ThreadCap t) slot extras \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<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 extras | TCBConfigure \<Rightarrow> decode_tcb_configure args (ThreadCap t) slot extras | TCBSetPriority \<Rightarrow> decode_set_priority args (ThreadCap t) slot extras | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args (ThreadCap t) slot extras | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args (ThreadCap t) slot extras | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args (ThreadCap t) slot extras | TCBSetSpace \<Rightarrow> decode_set_space args (ThreadCap t) slot extras | TCBSuspend \<Rightarrow> returnOk $ Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) extras | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<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 extras | TCBConfigure \<Rightarrow> decode_tcb_configure args (ThreadCap t) slot extras | TCBSetPriority \<Rightarrow> decode_set_priority args (ThreadCap t) slot extras | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args (ThreadCap t) slot extras | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args (ThreadCap t) slot extras | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer args (ThreadCap t) slot extras | TCBSetSpace \<Rightarrow> decode_set_space args (ThreadCap t) slot extras | TCBSuspend \<Rightarrow> returnOk $ Suspend $ obj_ref_of (ThreadCap t) | TCBResume \<Rightarrow> returnOk $ Resume $ obj_ref_of (ThreadCap t) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap t) extras | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base args (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> (gen_invocation_type label = InvalidInvocation \<longrightarrow> P s \<and> True) \<and> (gen_invocation_type label = UntypedRetype \<longrightarrow> P s \<and> True) \<and> (gen_invocation_type label = TCBReadRegisters \<longrightarrow> P s) \<and> (gen_invocation_type label = TCBWriteRegisters \<longrightarrow> P s) \<and> (gen_invocation_type label = TCBCopyRegisters \<longrightarrow> P s) \<and> (gen_invocation_type label = TCBConfigure \<longrightarrow> P s) \<and> (gen_invocation_type label = TCBSetPriority \<longrightarrow> P s) \<and> (gen_invocation_type label = TCBSetMCPriority \<longrightarrow> P s) \<and> (gen_invocation_type label = TCBSetSchedParams \<longrightarrow> P s) \<and> (gen_invocation_type label = TCBSetIPCBuffer \<longrightarrow> P s) \<and> (gen_invocation_type label = TCBSetSpace \<longrightarrow> P s) \<and> (gen_invocation_type label = TCBSuspend \<longrightarrow> P s) \<and> (gen_invocation_type label = TCBResume \<longrightarrow> P s) \<and> (gen_invocation_type label = TCBBindNotification \<longrightarrow> P s) \<and> (gen_invocation_type label = TCBUnbindNotification \<longrightarrow> P s) \<and> (gen_invocation_type label = TCBSetTLSBase \<longrightarrow> P s) \<and> (gen_invocation_type label = CNodeRevoke \<longrightarrow> P s \<and> True) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> P s \<and> True) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> P s \<and> True) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> P s \<and> True) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> P s \<and> True) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> P s \<and> True) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> P s \<and> True) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> P s \<and> True) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> P s \<and> True) \<and> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> P s \<and> True) \<and> (gen_invocation_type label = IRQAckIRQ \<longrightarrow> P s \<and> True) \<and> (gen_invocation_type label = IRQSetIRQHandler \<longrightarrow> P s \<and> True) \<and> (gen_invocation_type label = IRQClearIRQHandler \<longrightarrow> P s \<and> True) \<and> (gen_invocation_type label = DomainSetSet \<longrightarrow> P s \<and> True) proof (prove)
goal:
No subgoals!