theory Tcb_R

lemma decodeBindNotification_wf:
  "\<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t
         and (\<lambda>s. \<forall>x \<in> set extras. s \<turnstile>' (fst x) \<and> (\<forall>y \<in> zobj_refs' (fst x). ex_nonz_cap_to' y s))\<rbrace>
     decodeBindNotification (capability.ThreadCap t) extras
   \<lbrace>tcb_inv_wf'\<rbrace>,-" apply (simp add: decodeBindNotification_def whenE_def
             cong: list.case_cong split del: if_split) apply (rule hoare_pre) apply (wp getNotification_wp getObject_tcb_wp
        | wpc
        | simp add: threadGet_def getBoundNotification_def)+ apply (fastforce simp: valid_cap'_def[where c="capability.ThreadCap t"]
                         is_ntfn invs_def valid_state'_def valid_pspace'_def
                         projectKOs null_def pred_tcb_at'_def obj_at'_def
                   dest!: global'_no_ex_cap hd_in_set) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>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))\<rbrace> decodeBindNotification (capability.ThreadCap t) extras \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>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))\<rbrace> doE y <- if null extras then throwError Fault_H.syscall_error.TruncatedMessage else returnOk ();
ntfn <- liftE (getBoundNotification t);
y <- case ntfn of None \<Rightarrow> returnOk () | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation;
(ntfnPtr, rights) <- case fst (hd extras) of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation;
y <- if \<not> rights then throwError Fault_H.syscall_error.IllegalOperation else returnOk ();
notification <- liftE (getNotification ntfnPtr);
y <- case ntfnObj notification of Structures_H.ntfn.WaitingNtfn list \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfnBoundTCB notification of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation;
returnOk (tcbinvocation.NotificationControl t (Some ntfnPtr))
odE \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'4\<rbrace> doE y <- if null extras then throwError Fault_H.syscall_error.TruncatedMessage else returnOk ();
ntfn <- liftE (getBoundNotification t);
y <- case ntfn of None \<Rightarrow> returnOk () | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation;
(ntfnPtr, rights) <- case fst (hd extras) of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation;
y <- if \<not> rights then throwError Fault_H.syscall_error.IllegalOperation else returnOk ();
notification <- liftE (getNotification ntfnPtr);
y <- case ntfnObj notification of Structures_H.ntfn.WaitingNtfn list \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfnBoundTCB notification of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation;
returnOk (tcbinvocation.NotificationControl t (Some ntfnPtr))
odE \<lbrace>tcb_inv_wf'\<rbrace>, -
 2. \<And>s. (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 \<Longrightarrow> ?P'4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> tcb_at' t s \<and> ex_nonz_cap_to' t s \<and> (\<forall>x\<in>set extras. valid_cap' (fst x) s \<and> (\<forall>y\<in>zobj_refs' (fst x). ex_nonz_cap_to' y s)) \<Longrightarrow> \<not> null extras \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (tcbBoundNotification ta = None \<longrightarrow> (\<forall>x xa xb xc. fst (hd extras) = capability.NotificationCap x xa xb xc \<longrightarrow> xc \<longrightarrow> (\<forall>ntfn. ko_at' ntfn x s \<longrightarrow> (ntfnObj ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> ntfnBoundTCB ntfn = None \<longrightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) x s \<and> ex_nonz_cap_to' x s \<and> bound_tcb_at' ((=) None) t s) \<and> ((\<exists>x. ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x) \<longrightarrow> ntfnBoundTCB ntfn = None \<longrightarrow> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<and> (\<forall>q. ntfnObj ko \<noteq> Structures_H.ntfn.WaitingNtfn q)) x s \<and> ex_nonz_cap_to' x s \<and> bound_tcb_at' ((=) None) t s))))) proof (prove)
goal:
No subgoals!