theory Tcb_R

lemma decodeTCBInv_wf:
  "\<lbrace>invs' and tcb_at' t and cte_at' slot and ex_nonz_cap_to' t
         and (\<lambda>s. \<forall>x \<in> set extras. real_cte_at' (snd x) s
                          \<and> s \<turnstile>' fst x \<and> (\<forall>y \<in> zobj_refs' (fst x). ex_nonz_cap_to' y s))\<rbrace>
     decodeTCBInvocation label args (capability.ThreadCap t) slot extras
   \<lbrace>tcb_inv_wf'\<rbrace>,-" apply (simp add: decodeTCBInvocation_def Let_def
              cong: if_cong gen_invocation_labels.case_cong split del: if_split) apply (rule hoare_pre) apply (wpc, (wp decodeTCBConf_wf decodeReadReg_wf decodeWriteReg_wf decodeSetTLSBase_wf
             decodeCopyReg_wf decodeBindNotification_wf decodeUnbindNotification_wf)+) apply (clarsimp simp: real_cte_at') apply (fastforce simp: real_cte_at_not_tcb_at' objBits_defs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and cte_wp_at' (\<lambda>_. True) slot and ex_nonz_cap_to' t and (\<lambda>s. \<forall>x\<in>set extras. real_cte_at' (snd x) s \<and> valid_cap' (fst x) s \<and> (\<forall>y\<in>zobj_refs' (fst x). ex_nonz_cap_to' y s))\<rbrace> decodeTCBInvocation label args (capability.ThreadCap t) slot extras \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and cte_wp_at' (\<lambda>_. True) slot and ex_nonz_cap_to' t and (\<lambda>s. \<forall>x\<in>set extras. real_cte_at' (snd x) s \<and> valid_cap' (fst x) s \<and> (\<forall>y\<in>zobj_refs' (fst x). ex_nonz_cap_to' y s))\<rbrace> case gen_invocation_type label of TCBReadRegisters \<Rightarrow> decodeReadRegisters args (capability.ThreadCap t) | TCBWriteRegisters \<Rightarrow> decodeWriteRegisters args (capability.ThreadCap t) | TCBCopyRegisters \<Rightarrow> decodeCopyRegisters args (capability.ThreadCap t) (map fst extras) | TCBConfigure \<Rightarrow> decodeTCBConfigure args (capability.ThreadCap t) slot extras | TCBSetPriority \<Rightarrow> decodeSetPriority args (capability.ThreadCap t) extras | TCBSetMCPriority \<Rightarrow> decodeSetMCPriority args (capability.ThreadCap t) extras | TCBSetSchedParams \<Rightarrow> decodeSetSchedParams args (capability.ThreadCap t) extras | TCBSetIPCBuffer \<Rightarrow> decodeSetIPCBuffer args (capability.ThreadCap t) slot extras | TCBSetSpace \<Rightarrow> decodeSetSpace args (capability.ThreadCap t) slot extras | TCBSuspend \<Rightarrow> returnOk (tcbinvocation.Suspend t) | TCBResume \<Rightarrow> returnOk (tcbinvocation.Resume t) | TCBBindNotification \<Rightarrow> decodeBindNotification (capability.ThreadCap t) extras | TCBUnbindNotification \<Rightarrow> decodeUnbindNotification (capability.ThreadCap t) | TCBSetTLSBase \<Rightarrow> decodeSetTLSBase args (capability.ThreadCap t) | _ \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'32\<rbrace> case gen_invocation_type label of TCBReadRegisters \<Rightarrow> decodeReadRegisters args (capability.ThreadCap t) | TCBWriteRegisters \<Rightarrow> decodeWriteRegisters args (capability.ThreadCap t) | TCBCopyRegisters \<Rightarrow> decodeCopyRegisters args (capability.ThreadCap t) (map fst extras) | TCBConfigure \<Rightarrow> decodeTCBConfigure args (capability.ThreadCap t) slot extras | TCBSetPriority \<Rightarrow> decodeSetPriority args (capability.ThreadCap t) extras | TCBSetMCPriority \<Rightarrow> decodeSetMCPriority args (capability.ThreadCap t) extras | TCBSetSchedParams \<Rightarrow> decodeSetSchedParams args (capability.ThreadCap t) extras | TCBSetIPCBuffer \<Rightarrow> decodeSetIPCBuffer args (capability.ThreadCap t) slot extras | TCBSetSpace \<Rightarrow> decodeSetSpace args (capability.ThreadCap t) slot extras | TCBSuspend \<Rightarrow> returnOk (tcbinvocation.Suspend t) | TCBResume \<Rightarrow> returnOk (tcbinvocation.Resume t) | TCBBindNotification \<Rightarrow> decodeBindNotification (capability.ThreadCap t) extras | TCBUnbindNotification \<Rightarrow> decodeUnbindNotification (capability.ThreadCap t) | TCBSetTLSBase \<Rightarrow> decodeSetTLSBase args (capability.ThreadCap t) | _ \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>tcb_inv_wf'\<rbrace>, -
 2. \<And>s. (invs' and tcb_at' t and cte_wp_at' (\<lambda>_. True) slot and ex_nonz_cap_to' t and (\<lambda>s. \<forall>x\<in>set extras. real_cte_at' (snd x) s \<and> valid_cap' (fst x) s \<and> (\<forall>y\<in>zobj_refs' (fst x). ex_nonz_cap_to' y s))) s \<Longrightarrow> ?P'32 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and tcb_at' t and cte_wp_at' (\<lambda>_. True) slot and ex_nonz_cap_to' t and (\<lambda>s. \<forall>x\<in>set extras. real_cte_at' (snd x) s \<and> valid_cap' (fst x) s \<and> (\<forall>y\<in>zobj_refs' (fst x). ex_nonz_cap_to' y s))) s \<Longrightarrow> (gen_invocation_type label = InvalidInvocation \<longrightarrow> True) \<and> (gen_invocation_type label = UntypedRetype \<longrightarrow> True) \<and> (gen_invocation_type label = TCBReadRegisters \<longrightarrow> (invs' and tcb_at' t and ex_nonz_cap_to' t) s) \<and> (gen_invocation_type label = TCBWriteRegisters \<longrightarrow> (invs' and tcb_at' t and ex_nonz_cap_to' t) s) \<and> (gen_invocation_type label = TCBCopyRegisters \<longrightarrow> (invs' and tcb_at' t and ex_nonz_cap_to' t and (\<lambda>s. \<forall>x\<in>set (map fst extras). valid_cap' x s \<and> (\<forall>y\<in>zobj_refs' x. ex_nonz_cap_to' y s))) s) \<and> (gen_invocation_type label = TCBConfigure \<longrightarrow> (invs' and tcb_at' t and ex_nonz_cap_to' t and cte_wp_at' (\<lambda>_. True) slot and (\<lambda>s. \<forall>x\<in>set extras. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s \<and> t \<noteq> snd x \<and> t + 2 ^ cteSizeBits \<noteq> snd x)) s) \<and> (gen_invocation_type label = TCBSetPriority \<longrightarrow> (invs' and tcb_at' t and ex_nonz_cap_to' t) s) \<and> (gen_invocation_type label = TCBSetMCPriority \<longrightarrow> (invs' and tcb_at' t and ex_nonz_cap_to' t) s) \<and> (gen_invocation_type label = TCBSetSchedParams \<longrightarrow> (invs' and tcb_at' t and ex_nonz_cap_to' t) s) \<and> (gen_invocation_type label = TCBSetIPCBuffer \<longrightarrow> (invs' and tcb_at' t and ex_nonz_cap_to' t and cte_wp_at' (\<lambda>_. True) slot and (\<lambda>s. \<forall>v\<in>set extras. valid_cap' (fst v) s \<and> cte_wp_at' (\<lambda>_. True) (snd v) s)) s) \<and> (gen_invocation_type label = TCBSetSpace \<longrightarrow> (invs' and tcb_at' t and ex_nonz_cap_to' t and cte_wp_at' (\<lambda>_. True) slot and (\<lambda>s. \<forall>x\<in>set extras. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s \<and> t \<noteq> snd x \<and> t + 0x10 \<noteq> snd x)) s) \<and> (gen_invocation_type label = TCBSuspend \<longrightarrow> tcb_inv_wf' (tcbinvocation.Suspend t) s) \<and> (gen_invocation_type label = TCBResume \<longrightarrow> tcb_inv_wf' (tcbinvocation.Resume t) s) \<and> (gen_invocation_type label = TCBBindNotification \<longrightarrow> (invs' and tcb_at' t and ex_nonz_cap_to' t and (\<lambda>s. \<forall>x\<in>set extras. valid_cap' (fst x) s \<and> (\<forall>y\<in>zobj_refs' (fst x). ex_nonz_cap_to' y s))) s) \<and> (gen_invocation_type label = TCBUnbindNotification \<longrightarrow> (invs' and tcb_at' t and ex_nonz_cap_to' t) s) \<and> (gen_invocation_type label = TCBSetTLSBase \<longrightarrow> (invs' and tcb_at' t and ex_nonz_cap_to' 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) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; tcb_at' t s; cte_wp_at' (\<lambda>_. True) slot s; ex_nonz_cap_to' t s; \<forall>x\<in>set extras. real_cte_at' (snd x) s \<and> valid_cap' (fst x) s \<and> (\<forall>y\<in>zobj_refs' (fst x). ex_nonz_cap_to' y s)\<rbrakk> \<Longrightarrow> (gen_invocation_type label = TCBConfigure \<longrightarrow> (\<forall>x\<in>set extras. t \<noteq> snd x \<and> t + 2 ^ cteSizeBits \<noteq> snd x)) \<and> (gen_invocation_type label = TCBSetSpace \<longrightarrow> (\<forall>x\<in>set extras. t \<noteq> snd x \<and> t + 0x10 \<noteq> snd x)) proof (prove)
goal:
No subgoals!