theory Tcb_R

lemma decodeBindNotification_corres:
notes if_cong[cong] shows
  "\<lbrakk> list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<rbrakk> \<Longrightarrow>
    corres (ser \<oplus> tcbinv_relation)
      (invs and tcb_at t and (\<lambda>s. \<forall>x \<in> set extras. s \<turnstile> (fst x)))
      (invs' and tcb_at' t and (\<lambda>s. \<forall>x \<in> set extras'. s \<turnstile>' (fst x)))
     (decode_bind_notification (cap.ThreadCap t) extras)
     (decodeBindNotification (capability.ThreadCap t) extras')" apply (simp add: decode_bind_notification_def decodeBindNotification_def) apply (simp add: null_def returnOk_def) apply (rule corres_guard_imp) apply (rule corres_split_norE) apply (rule corres_trivial) apply (auto simp: returnOk_def whenE_def)[1] apply (rule_tac F="extras \<noteq> []" in corres_gen_asm) apply (rule corres_split_eqrE) apply simp apply (rule getBoundNotification_corres) apply (rule corres_split_norE) apply (rule corres_trivial, simp split: option.splits add: returnOk_def) apply (rule corres_splitEE'[where r'="\<lambda>rv rv'. ((fst rv) = (fst rv')) \<and> ((snd rv') = (AllowRead \<in> (snd rv)))"]) apply (rule corres_trivial, simp) apply (case_tac extras, simp, clarsimp simp: list_all2_Cons1) apply (fastforce split: cap.splits capability.splits simp: returnOk_def) apply (rule corres_split_norE) apply (rule corres_trivial, clarsimp simp: whenE_def returnOk_def) apply (clarsimp split del: if_split) apply (rule corres_splitEE[where r'=ntfn_relation]) apply simp apply (rule getNotification_corres) apply (rule corres_trivial, simp split del: if_split) apply (simp add: ntfn_relation_def
                          split: Structures_A.ntfn.splits Structures_H.ntfn.splits
                                 option.splits) apply wp+ apply (wp | simp add: whenE_def split del: if_split)+ apply (wp | wpc | simp)+ apply (simp | wp gbn_wp gbn_wp')+ apply (fastforce simp: valid_cap_def valid_cap'_def dest: hd_in_set)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (invs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) (decode_bind_notification (cap.ThreadCap t) extras) (decodeBindNotification (capability.ThreadCap t) extras') proof (prove)
goal (1 subgoal):
 1. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (invs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) (doE y <- whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> returnOk () | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
(ntfnptr, rights) <- case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
y <- whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
returnOk (tcb_invocation.NotificationControl t (Some ntfnptr))
odE) (doE y <- whenE (null extras') (throwError Fault_H.syscall_error.TruncatedMessage);
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 <- whenE (\<not> rights) (throwError Fault_H.syscall_error.IllegalOperation);
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) proof (prove)
goal (1 subgoal):
 1. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (invs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) (doE y <- whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
(ntfnptr, rights) <- case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
y <- whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some ntfnptr)))
odE) (doE y <- whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage);
ntfn <- liftE (getBoundNotification t);
y <- case ntfn of None \<Rightarrow> return (Inr ()) | 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 <- whenE (\<not> rights) (throwError Fault_H.syscall_error.IllegalOperation);
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;
return (Inr (tcbinvocation.NotificationControl t (Some ntfnPtr)))
odE) proof (prove)
goal (3 subgoals):
 1. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) ?Q4 ?Q'4 (doE y <- whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage);
nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
(ntfnptr, rights) <- case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
y <- whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some ntfnptr)))
odE) (doE y <- whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage);
ntfn <- liftE (getBoundNotification t);
y <- case ntfn of None \<Rightarrow> return (Inr ()) | 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 <- whenE (\<not> rights) (throwError Fault_H.syscall_error.IllegalOperation);
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;
return (Inr (tcbinvocation.NotificationControl t (Some ntfnPtr)))
odE)
 2. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) s\<rbrakk> \<Longrightarrow> ?Q4 s
 3. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) s\<rbrakk> \<Longrightarrow> ?Q'4 s proof (prove)
goal (6 subgoals):
 1. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> corres (ser \<oplus> dc) ?P8 ?P'8 (whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage)) (whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage))
 2. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) ?R8 ?R'8 (doE nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
(ntfnptr, rights) <- case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
y <- whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some ntfnptr)))
odE) (doE ntfn <- liftE (getBoundNotification t);
y <- case ntfn of None \<Rightarrow> return (Inr ()) | 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 <- whenE (\<not> rights) (throwError Fault_H.syscall_error.IllegalOperation);
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;
return (Inr (tcbinvocation.NotificationControl t (Some ntfnPtr)))
odE)
 3. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q8\<rbrace> whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. ?R8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q'8\<rbrace> whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. ?R'8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) s\<rbrakk> \<Longrightarrow> (?P8 and ?Q8) s
 6. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) s\<rbrakk> \<Longrightarrow> (?P'8 and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> corres (ser \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage)) (whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage))
 2. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) ?R8 ?R'8 (doE nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
(ntfnptr, rights) <- case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
y <- whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some ntfnptr)))
odE) (doE ntfn <- liftE (getBoundNotification t);
y <- case ntfn of None \<Rightarrow> return (Inr ()) | 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 <- whenE (\<not> rights) (throwError Fault_H.syscall_error.IllegalOperation);
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;
return (Inr (tcbinvocation.NotificationControl t (Some ntfnPtr)))
odE)
 3. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q8\<rbrace> whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. ?R8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q'8\<rbrace> whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. ?R'8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 6. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) ?R8 ?R'8 (doE nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
(ntfnptr, rights) <- case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
y <- whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some ntfnptr)))
odE) (doE ntfn <- liftE (getBoundNotification t);
y <- case ntfn of None \<Rightarrow> return (Inr ()) | 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 <- whenE (\<not> rights) (throwError Fault_H.syscall_error.IllegalOperation);
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;
return (Inr (tcbinvocation.NotificationControl t (Some ntfnPtr)))
odE)
 2. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q8\<rbrace> whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. ?R8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q'8\<rbrace> whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. ?R'8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 5. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) ?P41 ?R'8 (doE nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
(ntfnptr, rights) <- case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
y <- whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some ntfnptr)))
odE) (doE ntfn <- liftE (getBoundNotification t);
y <- case ntfn of None \<Rightarrow> return (Inr ()) | 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 <- whenE (\<not> rights) (throwError Fault_H.syscall_error.IllegalOperation);
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;
return (Inr (tcbinvocation.NotificationControl t (Some ntfnPtr)))
odE)
 2. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q8\<rbrace> whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. ?P41 and (\<lambda>s. extras \<noteq> [])\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q'8\<rbrace> whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. ?R'8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 5. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (8 subgoals):
 1. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> corres (ser \<oplus> (=)) ?P42 ?P'42 (liftE (get_bound_notification t)) (liftE (getBoundNotification t))
 2. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R42 nTFN) (?R'42 nTFN) (doE y <- case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
(ntfnptr, rights) <- case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
y <- whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some ntfnptr)))
odE) (doE y <- case nTFN of None \<Rightarrow> return (Inr ()) | 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 <- whenE (\<not> rights) (throwError Fault_H.syscall_error.IllegalOperation);
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;
return (Inr (tcbinvocation.NotificationControl t (Some ntfnPtr)))
odE)
 3. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q42\<rbrace> liftE (get_bound_notification t) \<lbrace>?R42\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42\<rbrace> liftE (getBoundNotification t) \<lbrace>?R'42\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q8\<rbrace> whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. ?P42 and ?Q42 and (\<lambda>s. extras \<noteq> [])\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q'8\<rbrace> whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. ?P'42 and ?Q'42\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 8. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (8 subgoals):
 1. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> corres (=) ?P42 ?P'42 (get_bound_notification t) (getBoundNotification t)
 2. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R42 nTFN) (?R'42 nTFN) (doE y <- case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
(ntfnptr, rights) <- case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
y <- whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some ntfnptr)))
odE) (doE y <- case nTFN of None \<Rightarrow> return (Inr ()) | 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 <- whenE (\<not> rights) (throwError Fault_H.syscall_error.IllegalOperation);
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;
return (Inr (tcbinvocation.NotificationControl t (Some ntfnPtr)))
odE)
 3. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q42\<rbrace> liftE (get_bound_notification t) \<lbrace>?R42\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42\<rbrace> liftE (getBoundNotification t) \<lbrace>?R'42\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q8\<rbrace> whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. ?P42 and ?Q42 and (\<lambda>s. extras \<noteq> [])\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q'8\<rbrace> whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. ?P'42 and ?Q'42\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 8. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R42 nTFN) (?R'42 nTFN) (doE y <- case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
(ntfnptr, rights) <- case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
y <- whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some ntfnptr)))
odE) (doE y <- case nTFN of None \<Rightarrow> return (Inr ()) | 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 <- whenE (\<not> rights) (throwError Fault_H.syscall_error.IllegalOperation);
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;
return (Inr (tcbinvocation.NotificationControl t (Some ntfnPtr)))
odE)
 2. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q42\<rbrace> liftE (get_bound_notification t) \<lbrace>?R42\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42\<rbrace> liftE (getBoundNotification t) \<lbrace>?R'42\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q8\<rbrace> whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at t and ?Q42 and (\<lambda>s. extras \<noteq> [])\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q'8\<rbrace> whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at' t and ?Q'42\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 7. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (10 subgoals):
 1. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (?P48 nTFN) (?P'48 nTFN) (case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case nTFN of None \<Rightarrow> return (Inr ()) | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation)
 2. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R48 nTFN) (?R'48 nTFN) (doE (ntfnptr, rights) <- case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
y <- whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some ntfnptr)))
odE) (doE (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 <- whenE (\<not> rights) (throwError Fault_H.syscall_error.IllegalOperation);
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;
return (Inr (tcbinvocation.NotificationControl t (Some ntfnPtr)))
odE)
 3. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>x. ?R48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>x. ?R'48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q42\<rbrace> liftE (get_bound_notification t) \<lbrace>\<lambda>nTFN. ?P48 nTFN and ?Q48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42\<rbrace> liftE (getBoundNotification t) \<lbrace>\<lambda>nTFN. ?P'48 nTFN and ?Q'48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q8\<rbrace> whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at t and ?Q42 and (\<lambda>s. extras \<noteq> [])\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q'8\<rbrace> whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at' t and ?Q'42\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 10. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (9 subgoals):
 1. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R48 nTFN) (?R'48 nTFN) (doE (ntfnptr, rights) <- case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
y <- whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some ntfnptr)))
odE) (doE (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 <- whenE (\<not> rights) (throwError Fault_H.syscall_error.IllegalOperation);
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;
return (Inr (tcbinvocation.NotificationControl t (Some ntfnPtr)))
odE)
 2. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>x. ?R48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>x. ?R'48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q42\<rbrace> liftE (get_bound_notification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42\<rbrace> liftE (getBoundNotification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q'48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q8\<rbrace> whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at t and ?Q42 and (\<lambda>s. extras \<noteq> [])\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q'8\<rbrace> whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at' t and ?Q'42\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 9. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (12 subgoals):
 1. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> corres (ser \<oplus> (\<lambda>rv rv'. fst rv = fst rv' \<and> snd rv' = (AllowRead \<in> snd rv))) (?P59 nTFN) (?P'59 nTFN) (case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case fst (hd extras') of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation)
 2. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R59 nTFN ntfnptr rights) (?R'59 nTFN x' y') (doE y <- whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some ntfnptr)))
odE) (doE y <- whenE (\<not> y') (throwError Fault_H.syscall_error.IllegalOperation);
notification <- liftE (getNotification x');
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;
return (Inr (tcbinvocation.NotificationControl t (Some x')))
odE)
 3. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 nTFN\<rbrace> case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). ?R59 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 nTFN\<rbrace> case fst (hd extras') of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). ?R'59 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>x. ?P59 nTFN and ?Q59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>x. ?P'59 nTFN and ?Q'59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q42\<rbrace> liftE (get_bound_notification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42\<rbrace> liftE (getBoundNotification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q'48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q8\<rbrace> whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at t and ?Q42 and (\<lambda>s. extras \<noteq> [])\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q'8\<rbrace> whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at' t and ?Q'42\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> corres (ser \<oplus> (\<lambda>rv rv'. fst rv = fst rv' \<and> snd rv' = (AllowRead \<in> snd rv))) (\<lambda>_. True) (\<lambda>_. True) (case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case fst (hd extras') of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation)
 2. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R59 nTFN ntfnptr rights) (?R'59 nTFN x' y') (doE y <- whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some ntfnptr)))
odE) (doE y <- whenE (\<not> y') (throwError Fault_H.syscall_error.IllegalOperation);
notification <- liftE (getNotification x');
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;
return (Inr (tcbinvocation.NotificationControl t (Some x')))
odE)
 3. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 nTFN\<rbrace> case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). ?R59 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 nTFN\<rbrace> case fst (hd extras') of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). ?R'59 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q42\<rbrace> liftE (get_bound_notification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42\<rbrace> liftE (getBoundNotification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q'48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q8\<rbrace> whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at t and ?Q42 and (\<lambda>s. extras \<noteq> [])\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q'8\<rbrace> whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at' t and ?Q'42\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>a aa b list ab ba zs. \<lbrakk>extras = (a, aa, b) # list; extras' = (ab, ba) # zs; cap_relation a ab; list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) list zs\<rbrakk> \<Longrightarrow> corres (ser \<oplus> (\<lambda>rv rv'. fst rv = fst rv' \<and> snd rv' = (AllowRead \<in> snd rv))) (\<lambda>_. True) (\<lambda>_. True) (case a of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation) (case ab of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation)
 2. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R59 nTFN ntfnptr rights) (?R'59 nTFN x' y') (doE y <- whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some ntfnptr)))
odE) (doE y <- whenE (\<not> y') (throwError Fault_H.syscall_error.IllegalOperation);
notification <- liftE (getNotification x');
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;
return (Inr (tcbinvocation.NotificationControl t (Some x')))
odE)
 3. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 nTFN\<rbrace> case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). ?R59 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 nTFN\<rbrace> case fst (hd extras') of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). ?R'59 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q42\<rbrace> liftE (get_bound_notification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42\<rbrace> liftE (getBoundNotification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q'48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q8\<rbrace> whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at t and ?Q42 and (\<lambda>s. extras \<noteq> [])\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q'8\<rbrace> whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at' t and ?Q'42\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R59 nTFN ntfnptr rights) (?R'59 nTFN x' y') (doE y <- whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some ntfnptr)))
odE) (doE y <- whenE (\<not> y') (throwError Fault_H.syscall_error.IllegalOperation);
notification <- liftE (getNotification x');
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;
return (Inr (tcbinvocation.NotificationControl t (Some x')))
odE)
 2. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 nTFN\<rbrace> case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). ?R59 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 nTFN\<rbrace> case fst (hd extras') of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). ?R'59 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q42\<rbrace> liftE (get_bound_notification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42\<rbrace> liftE (getBoundNotification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q'48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q8\<rbrace> whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at t and ?Q42 and (\<lambda>s. extras \<noteq> [])\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q'8\<rbrace> whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at' t and ?Q'42\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
A total of 11 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (?P266 nTFN ntfnptr rights) (?P'268 nTFN x' y') (whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation)) (whenE (\<not> y') (throwError Fault_H.syscall_error.IllegalOperation))
 2. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R265 nTFN ntfnptr rights x' y') (?R'265 nTFN ntfnptr rights x' y') (doE ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some ntfnptr)))
odE) (doE notification <- liftE (getNotification x');
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;
return (Inr (tcbinvocation.NotificationControl t (Some x')))
odE)
 3. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 nTFN ntfnptr rights\<rbrace> whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) \<lbrace>\<lambda>x. ?R265 nTFN ntfnptr rights x' y'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'269 nTFN x' y'\<rbrace> whenE (\<not> y') (throwError Fault_H.syscall_error.IllegalOperation) \<lbrace>\<lambda>x. ?R'265 nTFN ntfnptr rights x' y'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 nTFN\<rbrace> case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). ?P266 nTFN ntfnptr rights and ?Q267 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 nTFN\<rbrace> case fst (hd extras') of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). ?P'268 nTFN ntfnptr rights and ?Q'269 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q42\<rbrace> liftE (get_bound_notification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42\<rbrace> liftE (getBoundNotification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q'48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R265 nTFN ntfnptr rights x' y') (?R'265 nTFN ntfnptr rights x' y') (doE ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some ntfnptr)))
odE) (doE notification <- liftE (getNotification x');
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;
return (Inr (tcbinvocation.NotificationControl t (Some x')))
odE)
 2. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 nTFN ntfnptr rights\<rbrace> whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) \<lbrace>\<lambda>x. ?R265 nTFN ntfnptr rights x' y'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'269 nTFN x' y'\<rbrace> whenE (\<not> y') (throwError Fault_H.syscall_error.IllegalOperation) \<lbrace>\<lambda>x. ?R'265 nTFN ntfnptr rights x' y'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 nTFN\<rbrace> case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). (\<lambda>_. True) and ?Q267 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 nTFN\<rbrace> case fst (hd extras') of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). (\<lambda>_. True) and ?Q'269 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q42\<rbrace> liftE (get_bound_notification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42\<rbrace> liftE (getBoundNotification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q'48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q8\<rbrace> whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at t and ?Q42 and (\<lambda>s. extras \<noteq> [])\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>nTFN rights x'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R265 nTFN x' rights x' (AllowRead \<in> rights)) (?R'265 nTFN x' rights x' (AllowRead \<in> rights)) (doE ntfn <- liftE (get_notification x');
y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some x')))
odE) (doE notification <- liftE (getNotification x');
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;
return (Inr (tcbinvocation.NotificationControl t (Some x')))
odE)
 2. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 nTFN ntfnptr rights\<rbrace> whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) \<lbrace>\<lambda>x. ?R265 nTFN ntfnptr rights x' y'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'269 nTFN x' y'\<rbrace> whenE (\<not> y') (throwError Fault_H.syscall_error.IllegalOperation) \<lbrace>\<lambda>x. ?R'265 nTFN ntfnptr rights x' y'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 nTFN\<rbrace> case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). (\<lambda>_. True) and ?Q267 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 nTFN\<rbrace> case fst (hd extras') of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). (\<lambda>_. True) and ?Q'269 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q42\<rbrace> liftE (get_bound_notification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42\<rbrace> liftE (getBoundNotification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q'48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q8\<rbrace> whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at t and ?Q42 and (\<lambda>s. extras \<noteq> [])\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 13 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>nTFN rights x'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ntfn_relation) (?P291 nTFN rights x' x' (AllowRead \<in> rights)) (?P'289 nTFN rights x' x' (AllowRead \<in> rights)) (liftE (get_notification x')) (liftE (getNotification x'))
 2. \<And>nTFN rights x' ntfn notification. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; ntfn_relation ntfn notification\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R283 nTFN rights x' ntfn) (?R'283 nTFN rights x' notification) (doE y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some x')))
odE) (doE 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;
return (Inr (tcbinvocation.NotificationControl t (Some x')))
odE)
 3. \<And>nTFN rights x'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q290 nTFN rights x' x' (AllowRead \<in> rights)\<rbrace> liftE (get_notification x') \<lbrace>?R283 nTFN rights x'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>nTFN rights x'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'288 nTFN rights x' x' (AllowRead \<in> rights)\<rbrace> liftE (getNotification x') \<lbrace>?R'283 nTFN rights x'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 nTFN ntfnptr rights\<rbrace> whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) \<lbrace>\<lambda>x. ?P291 nTFN rights ntfnptr x' y' and ?Q290 nTFN rights ntfnptr x' y'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'269 nTFN x' y'\<rbrace> whenE (\<not> y') (throwError Fault_H.syscall_error.IllegalOperation) \<lbrace>\<lambda>x. ?P'289 nTFN rights ntfnptr x' y' and ?Q'288 nTFN rights ntfnptr x' y'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 nTFN\<rbrace> case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). (\<lambda>_. True) and ?Q267 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 nTFN\<rbrace> case fst (hd extras') of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). (\<lambda>_. True) and ?Q'269 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>nTFN rights x'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> corres ntfn_relation (?P291 nTFN rights x' x' (AllowRead \<in> rights)) (?P'289 nTFN rights x' x' (AllowRead \<in> rights)) (get_notification x') (getNotification x')
 2. \<And>nTFN rights x' ntfn notification. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; ntfn_relation ntfn notification\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R283 nTFN rights x' ntfn) (?R'283 nTFN rights x' notification) (doE y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some x')))
odE) (doE 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;
return (Inr (tcbinvocation.NotificationControl t (Some x')))
odE)
 3. \<And>nTFN rights x'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q290 nTFN rights x' x' (AllowRead \<in> rights)\<rbrace> liftE (get_notification x') \<lbrace>?R283 nTFN rights x'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>nTFN rights x'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'288 nTFN rights x' x' (AllowRead \<in> rights)\<rbrace> liftE (getNotification x') \<lbrace>?R'283 nTFN rights x'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 nTFN ntfnptr rights\<rbrace> whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) \<lbrace>\<lambda>x. ?P291 nTFN rights ntfnptr x' y' and ?Q290 nTFN rights ntfnptr x' y'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'269 nTFN x' y'\<rbrace> whenE (\<not> y') (throwError Fault_H.syscall_error.IllegalOperation) \<lbrace>\<lambda>x. ?P'289 nTFN rights ntfnptr x' y' and ?Q'288 nTFN rights ntfnptr x' y'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 nTFN\<rbrace> case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). (\<lambda>_. True) and ?Q267 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 nTFN\<rbrace> case fst (hd extras') of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). (\<lambda>_. True) and ?Q'269 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>nTFN rights x' ntfn notification. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; ntfn_relation ntfn notification\<rbrakk> \<Longrightarrow> corres (ser \<oplus> tcbinv_relation) (?R283 nTFN rights x' ntfn) (?R'283 nTFN rights x' notification) (doE y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some x')))
odE) (doE 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;
return (Inr (tcbinvocation.NotificationControl t (Some x')))
odE)
 2. \<And>nTFN rights x'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q290 nTFN rights x' x' (AllowRead \<in> rights)\<rbrace> liftE (get_notification x') \<lbrace>?R283 nTFN rights x'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>nTFN rights x'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'288 nTFN rights x' x' (AllowRead \<in> rights)\<rbrace> liftE (getNotification x') \<lbrace>?R'283 nTFN rights x'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 nTFN ntfnptr rights\<rbrace> whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) \<lbrace>\<lambda>x. ntfn_at x' and ?Q290 nTFN rights ntfnptr x' y'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'269 nTFN x' y'\<rbrace> whenE (\<not> y') (throwError Fault_H.syscall_error.IllegalOperation) \<lbrace>\<lambda>x. ntfn_at' x' and ?Q'288 nTFN rights ntfnptr x' y'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 nTFN\<rbrace> case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). (\<lambda>_. True) and ?Q267 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 nTFN\<rbrace> case fst (hd extras') of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). (\<lambda>_. True) and ?Q'269 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q42\<rbrace> liftE (get_bound_notification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>x' ntfn notification. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; ntfn_relation ntfn notification\<rbrakk> \<Longrightarrow> corres ((\<lambda>a aa. aa = syscall_error_map a) \<oplus> tcbinv_relation) (\<lambda>_. True) (\<lambda>_. True) (doE y <- case ntfn_obj ntfn of Structures_A.ntfn.WaitingNtfn list \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation;
return (Inr (tcb_invocation.NotificationControl t (Some x')))
odE) (doE 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;
return (Inr (tcbinvocation.NotificationControl t (Some x')))
odE)
 2. \<And>nTFN rights x'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q290 nTFN rights x' x' (AllowRead \<in> rights)\<rbrace> liftE (get_notification x') \<lbrace>\<lambda>ntfn _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>nTFN rights x'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'288 nTFN rights x' x' (AllowRead \<in> rights)\<rbrace> liftE (getNotification x') \<lbrace>\<lambda>notification _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 nTFN ntfnptr rights\<rbrace> whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) \<lbrace>\<lambda>x. ntfn_at x' and ?Q290 nTFN rights ntfnptr x' y'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'269 nTFN x' y'\<rbrace> whenE (\<not> y') (throwError Fault_H.syscall_error.IllegalOperation) \<lbrace>\<lambda>x. ntfn_at' x' and ?Q'288 nTFN rights ntfnptr x' y'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 nTFN\<rbrace> case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). (\<lambda>_. True) and ?Q267 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 nTFN\<rbrace> case fst (hd extras') of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). (\<lambda>_. True) and ?Q'269 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q42\<rbrace> liftE (get_bound_notification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>nTFN rights x'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q290 nTFN rights x' x' (AllowRead \<in> rights)\<rbrace> liftE (get_notification x') \<lbrace>\<lambda>ntfn _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>nTFN rights x'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'288 nTFN rights x' x' (AllowRead \<in> rights)\<rbrace> liftE (getNotification x') \<lbrace>\<lambda>notification _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 nTFN ntfnptr rights\<rbrace> whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) \<lbrace>\<lambda>x. ntfn_at x' and ?Q290 nTFN rights ntfnptr x' y'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'269 nTFN x' y'\<rbrace> whenE (\<not> y') (throwError Fault_H.syscall_error.IllegalOperation) \<lbrace>\<lambda>x. ntfn_at' x' and ?Q'288 nTFN rights ntfnptr x' y'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 nTFN\<rbrace> case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). (\<lambda>_. True) and ?Q267 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 nTFN\<rbrace> case fst (hd extras') of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). (\<lambda>_. True) and ?Q'269 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q42\<rbrace> liftE (get_bound_notification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42\<rbrace> liftE (getBoundNotification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q'48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 14 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> \<lbrace>?P'352 nTFN ntfnptr rights\<rbrace> whenE (AllowRead \<notin> rights) (throwError ExceptionTypes_A.syscall_error.IllegalOperation) \<lbrace>\<lambda>x s. ntfn_at x' s \<and> True \<and> True\<rbrace>, -
 2. \<And>nTFN ntfnptr rights x' y'. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []; fst (ntfnptr, rights) = fst (x', y') \<and> snd (x', y') = (AllowRead \<in> snd (ntfnptr, rights))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'269 nTFN x' y'\<rbrace> whenE (\<not> y') (throwError Fault_H.syscall_error.IllegalOperation) \<lbrace>\<lambda>x. ntfn_at' x' and (\<lambda>a. True \<and> True)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 nTFN\<rbrace> case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). (\<lambda>_. True) and (\<lambda>s. True \<and> ?P'352 nTFN ntfnptr rights s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 nTFN\<rbrace> case fst (hd extras') of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). (\<lambda>_. True) and ?Q'269 nTFN ntfnptr rights\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q42\<rbrace> liftE (get_bound_notification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42\<rbrace> liftE (getBoundNotification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q'48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q8\<rbrace> whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at t and ?Q42 and (\<lambda>s. extras \<noteq> [])\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q'8\<rbrace> whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at' t and ?Q'42\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 12 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P'383 nTFN\<rbrace> case fst (hd extras) of cap.NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights) s. AllowRead \<in> rights \<longrightarrow> ntfn_at ntfnptr s\<rbrace>, -
 2. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'59 nTFN\<rbrace> case fst (hd extras') of capability.NotificationCap ptr v12 v13 recv \<Rightarrow> returnOk (ptr, recv) | _ \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>(ntfnptr, rights). (\<lambda>_. True) and (\<lambda>s. True \<and> (if \<not> rights then \<lambda>a. True \<and> True else ntfn_at' ntfnptr and (\<lambda>a. True \<and> True)) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some x \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>s. True \<and> ?P'383 nTFN s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>nTFN. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'48 nTFN\<rbrace> case nTFN of None \<Rightarrow> return (Inr ()) | Some v11 \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q'59 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q42\<rbrace> liftE (get_bound_notification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42\<rbrace> liftE (getBoundNotification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and ?Q'48 nTFN\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q8\<rbrace> whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at t and ?Q42 and (\<lambda>s. extras \<noteq> [])\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q'8\<rbrace> whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at' t and ?Q'42\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 10. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P'745\<rbrace> get_bound_notification t \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> (\<forall>x xa xb. fst (hd extras) = cap.NotificationCap x xa xb \<longrightarrow> AllowRead \<in> xb \<longrightarrow> ntfn_at x s)\<rbrace>
 2. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; extras \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?Q'42\<rbrace> liftE (getBoundNotification t) \<lbrace>\<lambda>nTFN. (\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> (\<forall>x. fst (hd extras') = capability.ThreadCap x \<longrightarrow> True) \<and> (fst (hd extras') = capability.NullCap \<longrightarrow> True) \<and> (nTFN = None \<longrightarrow> (\<forall>x xa xb xc. fst (hd extras') = capability.NotificationCap x xa xb xc \<longrightarrow> (case (x, xc) of (ntfnptr, rights) \<Rightarrow> (\<lambda>_. True) and (\<lambda>s. True \<and> (if \<not> rights then \<lambda>a. True \<and> True else ntfn_at' ntfnptr and (\<lambda>a. True \<and> True)) s)) s) \<and> (\<forall>x. fst (hd extras') = capability.IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. fst (hd extras') = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> True) \<and> (fst (hd extras') = capability.DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb. fst (hd extras') = capability.Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. fst (hd extras') = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. fst (hd extras') = capability.ReplyCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb xc. fst (hd extras') = capability.UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb xc. fst (hd extras') = capability.CNodeCap x xa xb xc \<longrightarrow> True) \<and> (fst (hd extras') = capability.IRQControlCap \<longrightarrow> True)) \<and> (\<forall>x. nTFN = Some x \<longrightarrow> True))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q8\<rbrace> whenE (extras = []) (throwError ExceptionTypes_A.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at t and (\<lambda>s. True \<and> True \<and> True \<and> True \<and> True \<and> (fst (hd extras) = cap.NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. fst (hd extras) = cap.UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. fst (hd extras) = cap.EndpointCap x xa xb \<longrightarrow> True) \<and> ?P'745 s) and (\<lambda>s. extras \<noteq> [])\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras' \<Longrightarrow> \<lbrace>?Q'8\<rbrace> whenE (extras' = []) (throwError Fault_H.syscall_error.TruncatedMessage) \<lbrace>\<lambda>x. tcb_at' t and ?Q'42\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs and tcb_at t and (\<lambda>s. \<forall>x\<in>set extras. s \<turnstile> fst x)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 6. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; invs s \<and> tcb_at t s \<and> (\<forall>x\<in>set extras. s \<turnstile> fst x)\<rbrakk> \<Longrightarrow> extras \<noteq> [] \<longrightarrow> bound_tcb_at ((=) None) t s \<longrightarrow> (\<forall>x xa xb. fst (hd extras) = cap.NotificationCap x xa xb \<longrightarrow> AllowRead \<in> xb \<longrightarrow> ntfn_at x s)
 2. \<And>s. \<lbrakk>list_all2 (\<lambda>x y. cap_relation (fst x) (fst y)) extras extras'; (invs' and tcb_at' t and (\<lambda>s. \<forall>x\<in>set extras'. valid_cap' (fst x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> (if extras' = [] then \<lambda>s. True \<and> True else tcb_at' t and (\<lambda>s. bound_tcb_at' ((=) None) t s \<longrightarrow> (\<forall>x. (\<exists>xa xb. fst (hd extras') = capability.NotificationCap x xa xb True) \<longrightarrow> ntfn_at' x s))) s)) s proof (prove)
goal:
No subgoals!