theory Tcb_AC

lemma decode_bind_notification_authorised:
  "\<lbrace>K (is_subject aag t \<and> (\<forall>x \<in> set excaps. is_subject aag (fst (snd x)))
                        \<and> (\<forall>x \<in> set excaps. pas_cap_cur_auth aag (fst x)) )\<rbrace>
   decode_bind_notification (ThreadCap t) excaps
   \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -" unfolding decode_bind_notification_def authorised_tcb_inv_def apply clarsimp apply (wp gbn_wp get_simple_ko_wp whenE_throwError_wp | wpc | simp add:)+ apply (clarsimp dest!: hd_in_set) apply (drule_tac x="hd excaps"  in bspec, simp)+ apply (auto simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def AllowRecv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)))\<rbrace> decode_bind_notification (ThreadCap t) excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)))\<rbrace> case ThreadCap t of ThreadCap tcb \<Rightarrow> doE whenE (length excaps = 0) $ throwError TruncatedMessage;
nTFN <- liftE $ get_bound_notification tcb;
case nTFN of None \<Rightarrow> returnOk () | Some x \<Rightarrow> throwError IllegalOperation;
(ntfnptr, rights) <- case fst (hd excaps) of NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError IllegalOperation;
whenE (AllowRecv \<notin> rights) $ throwError IllegalOperation;
ntfn <- liftE $ get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (WaitingNtfn list, b) \<Rightarrow> throwError IllegalOperation | (_, None) \<Rightarrow> returnOk () | (_, Some a) \<Rightarrow> throwError IllegalOperation;
returnOk $ NotificationControl tcb (Some ntfnptr)
odE | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>rv _. case rv of WriteRegisters dest res values arch \<Rightarrow> is_subject aag dest | ReadRegisters src susp n arch \<Rightarrow> is_subject aag src | CopyRegisters dest src susp res frame int_regs arch \<Rightarrow> is_subject aag src \<and> is_subject aag dest | ThreadControl t sl ep mcp priority croot vroot buf \<Rightarrow> is_subject aag t \<and> (\<forall>(cap, slot)\<in>set_option croot \<union> set_option vroot \<union> (case buf of None \<Rightarrow> {} | Some x \<Rightarrow> (set_option \<circ> snd) x). pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)) | Suspend t \<Rightarrow> is_subject aag t | Resume t \<Rightarrow> is_subject aag t | NotificationControl t ntfn \<Rightarrow> is_subject aag t \<and> (case ntfn of None \<Rightarrow> True | Some a \<Rightarrow> \<forall>auth\<in>{Receive, Reset}. (pasSubject aag, auth, pasObjectAbs aag a) \<in> pasPolicy aag) | SetTLSBase tcb tls_base \<Rightarrow> is_subject aag tcb\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>y. is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x))\<rbrace> doE y <- whenE (excaps = []) (throwError TruncatedMessage);
nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> returnOk () | Some x \<Rightarrow> throwError IllegalOperation;
(ntfnptr, rights) <- case fst (hd excaps) of NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError IllegalOperation;
y <- whenE (AllowRecv \<notin> rights) (throwError IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of WaitingNtfn list \<Rightarrow> throwError IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError IllegalOperation;
returnOk (NotificationControl t (Some ntfnptr))
odE \<lbrace>\<lambda>rv _. case rv of WriteRegisters dest res values arch \<Rightarrow> is_subject aag dest | ReadRegisters src susp n arch \<Rightarrow> is_subject aag src | CopyRegisters dest src susp res frame int_regs arch \<Rightarrow> is_subject aag src \<and> is_subject aag dest | ThreadControl t sl ep mcp priority croot vroot buf \<Rightarrow> is_subject aag t \<and> (\<forall>(cap, slot)\<in>set_option croot \<union> set_option vroot \<union> (case buf of None \<Rightarrow> {} | Some x \<Rightarrow> (set_option \<circ> snd) x). pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)) | Suspend t \<Rightarrow> is_subject aag t | Resume t \<Rightarrow> is_subject aag t | NotificationControl t ntfn \<Rightarrow> is_subject aag t \<and> (case ntfn of None \<Rightarrow> True | Some a \<Rightarrow> \<forall>auth\<in>{Receive, Reset}. (pasSubject aag, auth, pasObjectAbs aag a) \<in> pasPolicy aag) | SetTLSBase tcb tls_base \<Rightarrow> is_subject aag tcb\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)) \<Longrightarrow> excaps \<noteq> [] \<longrightarrow> bound_tcb_at ((=) None) t s \<longrightarrow> (\<forall>x xa xb. fst (hd excaps) = NotificationCap x xa xb \<longrightarrow> AllowRecv \<in> xb \<longrightarrow> (\<exists>ntfn. ko_at (Notification ntfn) x s) \<longrightarrow> (pasSubject aag, Receive, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (pasSubject aag, Reset, pasObjectAbs aag x) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb ntfn. \<lbrakk>is_subject aag t; \<forall>x\<in>set excaps. is_subject aag (fst (snd x)); \<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x); hd excaps \<in> set excaps; bound_tcb_at ((=) None) t s; fst (hd excaps) = NotificationCap x xa xb; AllowRecv \<in> xb; ko_at (Notification ntfn) x s\<rbrakk> \<Longrightarrow> (pasSubject aag, Receive, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (pasSubject aag, Reset, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb ntfn. \<lbrakk>is_subject aag t; hd excaps \<in> set excaps; bound_tcb_at ((=) None) t s; fst (hd excaps) = NotificationCap x xa xb; AllowRecv \<in> xb; ko_at (Notification ntfn) x s; is_subject aag (fst (snd (hd excaps))); pas_cap_cur_auth aag (fst (hd excaps))\<rbrakk> \<Longrightarrow> (pasSubject aag, Receive, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (pasSubject aag, Reset, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!