theory Tcb_IF

lemma decode_tcb_invocation_authorised_extra:
  "\<lbrace>K (is_subject aag (fst slot))\<rbrace>
   decode_tcb_invocation label msg (ThreadCap t) slot excaps
   \<lbrace>\<lambda>rv s. authorised_tcb_inv_extra aag rv\<rbrace>, -" apply (simp add: authorised_tcb_inv_extra_def) apply (simp add: decode_tcb_invocation_def) apply (rule hoare_pre) apply (wp OR_choice_E_weak_wp
          | wpc | simp add: decode_read_registers_def
                            decode_write_registers_def
                            decode_copy_registers_def
                            decode_tcb_configure_def
                            decode_set_priority_def
                            decode_set_mcpriority_def
                            decode_set_sched_params_def
                            decode_set_ipc_buffer_def
                            decode_bind_notification_def
                            decode_unbind_notification_def
                            decode_set_tls_base_def
                            split_def decode_set_space_def
                 split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_subject aag (fst slot))\<rbrace> decode_tcb_invocation label msg (ThreadCap t) slot excaps \<lbrace>\<lambda>rv s. authorised_tcb_inv_extra aag rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>y. is_subject aag (fst slot)\<rbrace> decode_tcb_invocation label msg (ThreadCap t) slot excaps \<lbrace>\<lambda>rv s. case rv of ThreadControl x slot xa xb xc xd xe xf \<Rightarrow> is_subject aag (fst slot) | _ \<Rightarrow> True\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>y. is_subject aag (fst slot)\<rbrace> case gen_invocation_type label of TCBReadRegisters \<Rightarrow> decode_read_registers msg (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers msg (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers msg (ThreadCap t) $ map fst excaps | TCBConfigure \<Rightarrow> decode_tcb_configure msg (ThreadCap t) slot excaps | TCBSetPriority \<Rightarrow> decode_set_priority msg (ThreadCap t) slot excaps | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority msg (ThreadCap t) slot excaps | TCBSetSchedParams \<Rightarrow> decode_set_sched_params msg (ThreadCap t) slot excaps | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer msg (ThreadCap t) slot excaps | TCBSetSpace \<Rightarrow> decode_set_space msg (ThreadCap t) slot excaps | 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) excaps | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base msg (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>rv s. case rv of ThreadControl x slot xa xb xc xd xe xf \<Rightarrow> is_subject aag (fst slot) | _ \<Rightarrow> True\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case gen_invocation_type label of TCBReadRegisters \<Rightarrow> decode_read_registers msg (ThreadCap t) | TCBWriteRegisters \<Rightarrow> decode_write_registers msg (ThreadCap t) | TCBCopyRegisters \<Rightarrow> decode_copy_registers msg (ThreadCap t) $ map fst excaps | TCBConfigure \<Rightarrow> decode_tcb_configure msg (ThreadCap t) slot excaps | TCBSetPriority \<Rightarrow> decode_set_priority msg (ThreadCap t) slot excaps | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority msg (ThreadCap t) slot excaps | TCBSetSchedParams \<Rightarrow> decode_set_sched_params msg (ThreadCap t) slot excaps | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer msg (ThreadCap t) slot excaps | TCBSetSpace \<Rightarrow> decode_set_space msg (ThreadCap t) slot excaps | 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) excaps | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap t) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base msg (ThreadCap t) | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>rv s. case rv of ThreadControl x slot xa xb xc xd xe xf \<Rightarrow> is_subject aag (fst slot) | _ \<Rightarrow> True\<rbrace>, -
 2. \<And>s. is_subject aag (fst slot) \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!