theory Tcb_AC

lemma decode_set_ipc_buffer_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_set_ipc_buffer msg (ThreadCap t) slot excaps
   \<lbrace>\<lambda>rv _ :: det_ext state. authorised_tcb_inv aag rv\<rbrace>, -" unfolding decode_set_ipc_buffer_def authorised_tcb_inv_def apply (cases "excaps ! 0") apply (clarsimp cong: list.case_cong split del: if_split) apply (rule hoare_pre) apply (clarsimp simp: ball_Un aag_cap_auth_def split del: if_split split: prod.split
         | wp (once) derive_cap_obj_refs_auth derive_cap_untyped_range_subset derive_cap_clas
                     derive_cap_cli hoare_vcg_all_lift_R whenE_throwError_wp slot_long_running_inv
         | wpc)+ apply (cases excaps, simp) apply fastforce 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_set_ipc_buffer msg (ThreadCap t) slot 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> doE whenE (length msg = 0) $ throwError TruncatedMessage;
whenE (length excaps = 0) $ throwError TruncatedMessage;
buffer <- returnOk $ data_to_vref $ msg ! 0;
(bcap, bslot) <- returnOk $ excaps ! 0;
newbuf <- if buffer = 0 then returnOk None else doE buffer_cap <- derive_cap bslot bcap;
check_valid_ipc_buffer buffer buffer_cap;
returnOk $ Some (buffer_cap, bslot)
odE;
returnOk $ ThreadControl (obj_ref_of (ThreadCap t)) slot None None None None None (Some (buffer, newbuf))
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>a b c. excaps ! 0 = (a, b, c) \<Longrightarrow> \<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> doE whenE (length msg = 0) $ throwError TruncatedMessage;
whenE (length excaps = 0) $ throwError TruncatedMessage;
buffer <- returnOk $ data_to_vref $ msg ! 0;
(bcap, bslot) <- returnOk $ excaps ! 0;
newbuf <- if buffer = 0 then returnOk None else doE buffer_cap <- derive_cap bslot bcap;
check_valid_ipc_buffer buffer buffer_cap;
returnOk $ Some (buffer_cap, bslot)
odE;
returnOk $ ThreadControl (obj_ref_of (ThreadCap t)) slot None None None None None (Some (buffer, newbuf))
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>a b c. excaps ! 0 = (a, b, c) \<Longrightarrow> \<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 (msg = []) (throwError TruncatedMessage);
y <- whenE (excaps = []) (throwError TruncatedMessage);
newbuf <- if data_to_vref (msg ! 0) = 0 then returnOk None else doE buffer_cap <- derive_cap (b, c) a;
y <- check_valid_ipc_buffer (data_to_vref (msg ! 0)) buffer_cap;
returnOk (Some (buffer_cap, b, c))
odE;
returnOk (ThreadControl t slot None None None None None (Some (data_to_vref (msg ! 0), newbuf)))
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 (2 subgoals):
 1. \<And>a b c. excaps ! 0 = (a, b, c) \<Longrightarrow> \<lbrace>?P'4 a b c\<rbrace> doE y <- whenE (msg = []) (throwError TruncatedMessage);
y <- whenE (excaps = []) (throwError TruncatedMessage);
newbuf <- if data_to_vref (msg ! 0) = 0 then returnOk None else doE buffer_cap <- derive_cap (b, c) a;
y <- check_valid_ipc_buffer (data_to_vref (msg ! 0)) buffer_cap;
returnOk (Some (buffer_cap, b, c))
odE;
returnOk (ThreadControl t slot None None None None None (Some (data_to_vref (msg ! 0), newbuf)))
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>, -
 2. \<And>a b c s. \<lbrakk>excaps ! 0 = (a, b, c); 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))\<rbrakk> \<Longrightarrow> ?P'4 a b c s proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>excaps ! 0 = (a, b, c); is_subject aag t; \<forall>x\<in>set excaps. is_subject aag (fst (snd x)); \<forall>x\<in>set excaps. (\<forall>xa\<in>obj_refs_ac (fst x). \<forall>auth\<in>cap_auth_conferred (fst x). (pasSubject aag, auth, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst x). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (fst x) \<and> cap_links_irq aag (pasSubject aag) (fst x); msg \<noteq> []; excaps \<noteq> []; data_to_vref (msg ! 0) \<noteq> 0\<rbrakk> \<Longrightarrow> (\<forall>r\<in>obj_refs_ac a. \<forall>auth\<in>cap_auth_conferred a. (pasSubject aag, auth, pasObjectAbs aag r) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range a. (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) a \<and> cap_links_irq aag (pasSubject aag) a \<and> is_subject aag b proof (prove)
goal (1 subgoal):
 1. \<And>a b c aa list. \<lbrakk>excaps ! 0 = (a, b, c); is_subject aag t; \<forall>x\<in>set excaps. is_subject aag (fst (snd x)); \<forall>x\<in>set excaps. (\<forall>xa\<in>obj_refs_ac (fst x). \<forall>auth\<in>cap_auth_conferred (fst x). (pasSubject aag, auth, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (fst x). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (fst x) \<and> cap_links_irq aag (pasSubject aag) (fst x); msg \<noteq> []; excaps \<noteq> []; data_to_vref (msg ! 0) \<noteq> 0; excaps = aa # list\<rbrakk> \<Longrightarrow> (\<forall>r\<in>obj_refs_ac a. \<forall>auth\<in>cap_auth_conferred a. (pasSubject aag, auth, pasObjectAbs aag r) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range a. (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) a \<and> cap_links_irq aag (pasSubject aag) a \<and> is_subject aag b proof (prove)
goal:
No subgoals!