theory Tcb_AC

lemma decode_registers_authorised:
  "\<lbrace>K (is_subject aag t)\<rbrace> decode_read_registers msg (ThreadCap t) \<lbrace>\<lambda>rv s. authorised_tcb_inv aag rv\<rbrace>, -"
  "\<lbrace>K (is_subject aag t)\<rbrace> decode_write_registers msg (ThreadCap t) \<lbrace>\<lambda>rv s. authorised_tcb_inv aag rv\<rbrace>, -"
  "\<lbrace>pas_refined aag and K (is_subject aag t \<and> (\<forall>(cap, slot) \<in> set excaps. pas_cap_cur_auth aag cap
                                                                        \<and> is_subject aag (fst slot)))\<rbrace>
   decode_copy_registers msg (ThreadCap t) (map fst excaps)
   \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, -" unfolding decode_read_registers_def decode_write_registers_def
            decode_copy_registers_def authorised_tcb_inv_def apply (simp_all cong: list.case_cong) apply wpsimp+ apply (clarsimp simp: cap_auth_conferred_def pas_refined_all_auth_is_owns aag_cap_auth_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_subject aag t)\<rbrace> decode_read_registers msg (ThreadCap t) \<lbrace>\<lambda>rv s. authorised_tcb_inv aag rv\<rbrace>, - &&& \<lbrace>K (is_subject aag t)\<rbrace> decode_write_registers msg (ThreadCap t) \<lbrace>\<lambda>rv s. authorised_tcb_inv aag rv\<rbrace>, - &&& \<lbrace>pas_refined aag and K (is_subject aag t \<and> (\<forall>(cap, slot)\<in>set excaps. pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)))\<rbrace> decode_copy_registers msg (ThreadCap t) (map fst excaps) \<lbrace>\<lambda>rv _. authorised_tcb_inv aag rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_subject aag t)\<rbrace> case msg of [] \<Rightarrow> throwError TruncatedMessage | [flags] \<Rightarrow> throwError TruncatedMessage | flags # n # x \<Rightarrow> doE range_check n 1 $ word_of_nat (length frameRegisters + length gpRegisters);
p <- case ThreadCap t of ThreadCap p \<Rightarrow> returnOk p;
self <- liftE $ gets cur_thread;
whenE (p = self) $ throwError IllegalOperation;
returnOk $ ReadRegisters p (flags !! 0) n ArchDefaultExtraRegisters
odE \<lbrace>\<lambda>rv s. 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>, - &&& \<lbrace>K (is_subject aag t)\<rbrace> case msg of [] \<Rightarrow> throwError TruncatedMessage | [flags] \<Rightarrow> throwError TruncatedMessage | flags # n # values \<Rightarrow> doE whenE (length values < unat n) $ throwError TruncatedMessage;
p <- case ThreadCap t of ThreadCap p \<Rightarrow> returnOk p;
self <- liftE $ gets cur_thread;
whenE (p = self) $ throwError IllegalOperation;
returnOk $ WriteRegisters p (flags !! 0) (take (unat n) values) ArchDefaultExtraRegisters
odE \<lbrace>\<lambda>rv s. 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>, - &&& \<lbrace>pas_refined aag and K (is_subject aag t \<and> (\<forall>(cap, slot)\<in>set excaps. pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)))\<rbrace> case msg of [] \<Rightarrow> throwError TruncatedMessage | flags # x \<Rightarrow> doE suspend_source <- returnOk (flags !! 0);
resume_target <- returnOk (flags !! 1);
transfer_frame <- returnOk (flags !! 2);
transfer_integer <- returnOk (flags !! 3);
whenE (map fst excaps = []) $ throwError TruncatedMessage;
src_tcb <- case map fst excaps of [] \<Rightarrow> throwError $ InvalidCapability 1 | ThreadCap p # x \<Rightarrow> returnOk p | _ # x \<Rightarrow> throwError $ InvalidCapability 1;
p <- case ThreadCap t of ThreadCap p \<Rightarrow> returnOk p;
returnOk $ CopyRegisters p src_tcb suspend_source resume_target transfer_frame transfer_integer ArchDefaultExtraRegisters
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 (3 subgoals):
 1. \<lbrace>\<lambda>y. is_subject aag t\<rbrace> case msg of [] \<Rightarrow> throwError TruncatedMessage | [flags] \<Rightarrow> throwError TruncatedMessage | flags # n # x \<Rightarrow> doE y <- range_check n 1 (word_of_nat (length frameRegisters) + word_of_nat (length gpRegisters));
self <- liftE (gets cur_thread);
y <- whenE (t = self) (throwError IllegalOperation);
returnOk (ReadRegisters t (flags !! 0) n ArchDefaultExtraRegisters)
odE \<lbrace>\<lambda>rv s. 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>, -
 2. \<lbrace>\<lambda>y. is_subject aag t\<rbrace> case msg of [] \<Rightarrow> throwError TruncatedMessage | [flags] \<Rightarrow> throwError TruncatedMessage | flags # n # values \<Rightarrow> doE y <- whenE (length values < unat n) (throwError TruncatedMessage);
self <- liftE (gets cur_thread);
y <- whenE (t = self) (throwError IllegalOperation);
returnOk (WriteRegisters t (flags !! 0) (take (unat n) values) ArchDefaultExtraRegisters)
odE \<lbrace>\<lambda>rv s. 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>, -
 3. \<lbrace>pas_refined aag and (\<lambda>y. is_subject aag t \<and> (\<forall>x\<in>set excaps. case x of (cap, slot) \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)))\<rbrace> case msg of [] \<Rightarrow> throwError TruncatedMessage | flags # x \<Rightarrow> doE y <- whenE (excaps = []) (throwError TruncatedMessage);
src_tcb <- case map fst excaps of [] \<Rightarrow> throwError (InvalidCapability (Suc 0)) | ThreadCap xa # x \<Rightarrow> returnOk xa | _ # x \<Rightarrow> throwError $ InvalidCapability 1;
returnOk (CopyRegisters t src_tcb (flags !! 0) (flags !! Suc 0) (flags !! 2) (flags !! 3) ArchDefaultExtraRegisters)
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 x xa aa b zs xd. \<lbrakk>pas_refined aag s; is_subject aag t; msg = x # xa; excaps = (ThreadCap xd, aa, b) # zs; pas_cap_cur_auth aag (ThreadCap xd); is_subject aag aa; \<forall>x\<in>set zs. case x of (cap, slot) \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> is_subject aag xd proof (prove)
goal:
No subgoals!