theory Tcb_AC

lemma decode_tcb_invocation_authorised:
  "\<lbrace>invs and pas_refined aag
         and K (is_subject aag t \<and> (\<forall>x \<in> set excaps. is_subject aag (fst (snd x)))
                                 \<and> (\<forall>x \<in> set excaps. pas_cap_cur_auth aag (fst x)))\<rbrace>
   decode_tcb_invocation label msg (ThreadCap t) slot excaps
   \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -" unfolding decode_tcb_invocation_def apply (rule hoare_pre) apply wpc apply (wp decode_registers_authorised decode_tcb_configure_authorised
            decode_set_priority_authorised decode_set_mcpriority_authorised
            decode_set_sched_params_authorised
            decode_set_ipc_buffer_authorised decode_set_space_authorised
            decode_bind_notification_authorised
            decode_unbind_notification_authorised
            decode_set_tls_base_authorised)+ by (auto iff: authorised_tcb_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and pas_refined aag and K (is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)))\<rbrace> decode_tcb_invocation label msg (ThreadCap t) slot excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and pas_refined aag and K (is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)))\<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 _. authorised_tcb_inv aag rv\<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 _. authorised_tcb_inv aag rv\<rbrace>, -
 2. \<And>s. (invs and pas_refined aag and K (is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)))) s \<Longrightarrow> ?P' s proof (prove)
goal (31 subgoals):
 1. gen_invocation_type label = InvalidInvocation \<Longrightarrow> \<lbrace>?R64\<rbrace> throwError IllegalOperation \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -
 2. gen_invocation_type label = UntypedRetype \<Longrightarrow> \<lbrace>?R63\<rbrace> throwError IllegalOperation \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -
 3. gen_invocation_type label = TCBReadRegisters \<Longrightarrow> \<lbrace>?R62\<rbrace> decode_read_registers msg (ThreadCap t) \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -
 4. gen_invocation_type label = TCBWriteRegisters \<Longrightarrow> \<lbrace>?R61\<rbrace> decode_write_registers msg (ThreadCap t) \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -
 5. gen_invocation_type label = TCBCopyRegisters \<Longrightarrow> \<lbrace>?R60\<rbrace> decode_copy_registers msg (ThreadCap t) $ map fst excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -
 6. gen_invocation_type label = TCBConfigure \<Longrightarrow> \<lbrace>?R59\<rbrace> decode_tcb_configure msg (ThreadCap t) slot excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -
 7. gen_invocation_type label = TCBSetPriority \<Longrightarrow> \<lbrace>?R58\<rbrace> decode_set_priority msg (ThreadCap t) slot excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -
 8. gen_invocation_type label = TCBSetMCPriority \<Longrightarrow> \<lbrace>?R57\<rbrace> decode_set_mcpriority msg (ThreadCap t) slot excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -
 9. gen_invocation_type label = TCBSetSchedParams \<Longrightarrow> \<lbrace>?R56\<rbrace> decode_set_sched_params msg (ThreadCap t) slot excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -
 10. gen_invocation_type label = TCBSetIPCBuffer \<Longrightarrow> \<lbrace>?R55\<rbrace> decode_set_ipc_buffer msg (ThreadCap t) slot excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -
A total of 31 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and pas_refined aag and K (is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)))) s \<Longrightarrow> (gen_invocation_type label = InvalidInvocation \<longrightarrow> True) \<and> (gen_invocation_type label = UntypedRetype \<longrightarrow> True) \<and> (gen_invocation_type label = TCBReadRegisters \<longrightarrow> K (is_subject aag t) s) \<and> (gen_invocation_type label = TCBWriteRegisters \<longrightarrow> K (is_subject aag t) s) \<and> (gen_invocation_type label = TCBCopyRegisters \<longrightarrow> (pas_refined aag and K (is_subject aag t \<and> (\<forall>(cap, slot)\<in>set excaps. pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)))) s) \<and> (gen_invocation_type label = TCBConfigure \<longrightarrow> K (is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x))) s) \<and> (gen_invocation_type label = TCBSetPriority \<longrightarrow> K (is_subject aag t) s) \<and> (gen_invocation_type label = TCBSetMCPriority \<longrightarrow> K (is_subject aag t) s) \<and> (gen_invocation_type label = TCBSetSchedParams \<longrightarrow> K (is_subject aag t) s) \<and> (gen_invocation_type label = TCBSetIPCBuffer \<longrightarrow> K (is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x))) s) \<and> (gen_invocation_type label = TCBSetSpace \<longrightarrow> K (is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x))) s) \<and> (gen_invocation_type label = TCBSuspend \<longrightarrow> authorised_tcb_inv aag (Suspend $ obj_ref_of (ThreadCap t))) \<and> (gen_invocation_type label = TCBResume \<longrightarrow> authorised_tcb_inv aag (Resume $ obj_ref_of (ThreadCap t))) \<and> (gen_invocation_type label = TCBBindNotification \<longrightarrow> K (is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x))) s) \<and> (gen_invocation_type label = TCBUnbindNotification \<longrightarrow> K (is_subject aag t) s) \<and> (gen_invocation_type label = TCBSetTLSBase \<longrightarrow> K (is_subject aag t) s) \<and> (gen_invocation_type label = CNodeRevoke \<longrightarrow> True) \<and> (gen_invocation_type label = CNodeDelete \<longrightarrow> True) \<and> (gen_invocation_type label = CNodeCancelBadgedSends \<longrightarrow> True) \<and> (gen_invocation_type label = CNodeCopy \<longrightarrow> True) \<and> (gen_invocation_type label = CNodeMint \<longrightarrow> True) \<and> (gen_invocation_type label = CNodeMove \<longrightarrow> True) \<and> (gen_invocation_type label = CNodeMutate \<longrightarrow> True) \<and> (gen_invocation_type label = CNodeRotate \<longrightarrow> True) \<and> (gen_invocation_type label = CNodeSaveCaller \<longrightarrow> True) \<and> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> True) \<and> (gen_invocation_type label = IRQAckIRQ \<longrightarrow> True) \<and> (gen_invocation_type label = IRQSetIRQHandler \<longrightarrow> True) \<and> (gen_invocation_type label = IRQClearIRQHandler \<longrightarrow> True) \<and> (gen_invocation_type label = DomainSetSet \<longrightarrow> True)