theory Tcb_AI

lemma decode_bind_notification_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>
     decode_bind_notification (cap.ThreadCap t) extras
   \<lbrace>tcb_inv_wf\<rbrace>,-" apply (simp add: decode_bind_notification_def whenE_def
             cong: list.case_cong split del: if_split) apply (rule hoare_pre) apply (wp get_simple_ko_wp gbn_wp | wpc)+ apply (fastforce simp: valid_cap_def[where c="cap.ThreadCap t" for t] is_ntfn invs_def
                    valid_state_def valid_pspace_def
             elim!: obj_at_weakenE
             dest!: idle_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. s \<turnstile> fst x \<and> (\<forall>y\<in>zobj_refs (fst x). ex_nonz_cap_to y s))\<rbrace> decode_bind_notification (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. s \<turnstile> fst x \<and> (\<forall>y\<in>zobj_refs (fst x). ex_nonz_cap_to y s))\<rbrace> doE y <- if extras = [] then throwError TruncatedMessage else returnOk ();
nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> returnOk () | Some x \<Rightarrow> throwError IllegalOperation;
(ntfnptr, rights) <- case fst (hd extras) of NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError IllegalOperation;
y <- if AllowRecv \<notin> rights then throwError IllegalOperation else returnOk ();
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of WaitingNtfn list \<Rightarrow> throwError IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError IllegalOperation;
returnOk (NotificationControl t (Some ntfnptr))
odE \<lbrace>tcb_inv_wf\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> doE y <- if extras = [] then throwError TruncatedMessage else returnOk ();
nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> returnOk () | Some x \<Rightarrow> throwError IllegalOperation;
(ntfnptr, rights) <- case fst (hd extras) of NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError IllegalOperation;
y <- if AllowRecv \<notin> rights then throwError IllegalOperation else returnOk ();
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of WaitingNtfn list \<Rightarrow> throwError IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError IllegalOperation;
returnOk (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. s \<turnstile> fst x \<and> (\<forall>y\<in>zobj_refs (fst x). ex_nonz_cap_to y s))) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. (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))) s \<Longrightarrow> True \<and> True \<and> (extras = [] \<longrightarrow> True) \<and> (extras \<noteq> [] \<longrightarrow> (\<forall>ntfn. bound_tcb_at ((=) ntfn) t s \<longrightarrow> True \<and> True \<and> (fst (hd extras) = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. fst (hd extras) = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. fst (hd extras) = EndpointCap x xa xb \<longrightarrow> True) \<and> (ntfn = None \<longrightarrow> (\<forall>x xa xb. fst (hd extras) = NotificationCap x xa xb \<longrightarrow> (\<forall>xa xc. (x, xb) = (xa, xc) \<longrightarrow> True \<and> True \<and> (AllowRecv \<notin> xc \<longrightarrow> True) \<and> (\<not> AllowRecv \<notin> xc \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) xa s \<longrightarrow> True \<and> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> (ntfn_bound_tcb ntfn = None \<longrightarrow> tcb_inv_wf (NotificationControl t (Some xa)) s) \<and> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> True)) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> True) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> (ntfn_bound_tcb ntfn = None \<longrightarrow> tcb_inv_wf (NotificationControl t (Some xa)) s) \<and> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> True)))))) \<and> (\<forall>x xa xb. fst (hd extras) = ReplyCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. fst (hd extras) = CNodeCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. fst (hd extras) = ThreadCap x \<longrightarrow> True) \<and> (fst (hd extras) = DomainCap \<longrightarrow> True) \<and> (fst (hd extras) = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. fst (hd extras) = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. fst (hd extras) = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. fst (hd extras) = ArchObjectCap x \<longrightarrow> True)) \<and> (\<forall>x. ntfn = Some x \<longrightarrow> True))) proof (prove)
goal:
No subgoals!