theory Tcb_AC

lemma decode_set_space_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_space ws (ThreadCap t) slot excaps
   \<lbrace>\<lambda>rv _ :: det_ext state. authorised_tcb_inv aag rv\<rbrace>, -" unfolding decode_set_space_def authorised_tcb_inv_def apply (rule hoare_pre) apply (simp cong: list.case_cong split del: if_split) apply (clarsimp simp: ball_Un split del: if_split
         | wp (once) derive_cap_obj_refs_auth derive_cap_untyped_range_subset derive_cap_clas
                     derive_cap_cli hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R
                     whenE_throwError_wp slot_long_running_inv)+ apply (clarsimp simp: not_less all_set_conv_all_nth dest!: P_0_1_spec) apply (auto simp: aag_cap_auth_def update_cap_cli
             intro: update_cap_obj_refs_subset
             dest!: update_cap_cap_auth_conferred_subset) 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_space ws (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 ws < 3 \<or> length excaps < 2) $ throwError TruncatedMessage;
fault_ep <- returnOk $ ws ! 0;
croot_data <- returnOk $ ws ! 1;
vroot_data <- returnOk $ ws ! 2;
croot_arg <- returnOk $ excaps ! 0;
vroot_arg <- returnOk $ excaps ! 1;
can_chg_cr <- liftE $ liftM Not $ slot_cap_long_running_delete $ get_tcb_ctable_ptr $ obj_ref_of (ThreadCap t);
can_chg_vr <- liftE $ liftM Not $ slot_cap_long_running_delete $ get_tcb_vtable_ptr $ obj_ref_of (ThreadCap t);
unlessE (can_chg_cr \<and> can_chg_vr) $ throwError IllegalOperation;
croot_cap <- returnOk $ fst croot_arg;
croot_slot <- returnOk $ snd croot_arg;
croot_cap' <- derive_cap croot_slot $ (if croot_data = 0 then id else update_cap_data False croot_data) croot_cap;
unlessE (is_cnode_cap croot_cap') $ throwError IllegalOperation;
croot <- returnOk (croot_cap', croot_slot);
vroot_cap <- returnOk $ fst vroot_arg;
vroot_slot <- returnOk $ snd vroot_arg;
vroot_cap' <- derive_cap vroot_slot $ (if vroot_data = 0 then id else update_cap_data False vroot_data) vroot_cap;
unlessE (is_valid_vtable_root vroot_cap') $ throwError IllegalOperation;
vroot <- returnOk (vroot_cap', vroot_slot);
returnOk $ ThreadControl (obj_ref_of (ThreadCap t)) slot (Some (to_bl fault_ep)) None None (Some croot) (Some vroot) None
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. \<lbrace>?P'\<rbrace> doE whenE (length ws < 3 \<or> length excaps < 2) $ throwError TruncatedMessage;
fault_ep <- returnOk $ ws ! 0;
croot_data <- returnOk $ ws ! 1;
vroot_data <- returnOk $ ws ! 2;
croot_arg <- returnOk $ excaps ! 0;
vroot_arg <- returnOk $ excaps ! 1;
can_chg_cr <- liftE $ liftM Not $ slot_cap_long_running_delete $ get_tcb_ctable_ptr $ obj_ref_of (ThreadCap t);
can_chg_vr <- liftE $ liftM Not $ slot_cap_long_running_delete $ get_tcb_vtable_ptr $ obj_ref_of (ThreadCap t);
unlessE (can_chg_cr \<and> can_chg_vr) $ throwError IllegalOperation;
croot_cap <- returnOk $ fst croot_arg;
croot_slot <- returnOk $ snd croot_arg;
croot_cap' <- derive_cap croot_slot $ (if croot_data = 0 then id else update_cap_data False croot_data) croot_cap;
unlessE (is_cnode_cap croot_cap') $ throwError IllegalOperation;
croot <- returnOk (croot_cap', croot_slot);
vroot_cap <- returnOk $ fst vroot_arg;
vroot_slot <- returnOk $ snd vroot_arg;
vroot_cap' <- derive_cap vroot_slot $ (if vroot_data = 0 then id else update_cap_data False vroot_data) vroot_cap;
unlessE (is_valid_vtable_root vroot_cap') $ throwError IllegalOperation;
vroot <- returnOk (vroot_cap', vroot_slot);
returnOk $ ThreadControl (obj_ref_of (ThreadCap t)) slot (Some (to_bl fault_ep)) None None (Some croot) (Some vroot) None
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>s. 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))) s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> doE y <- whenE (length ws < 3 \<or> length excaps < 2) (throwError TruncatedMessage);
can_chg_cr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_ctable_ptr t)));
can_chg_vr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_vtable_ptr t)));
y <- unlessE (can_chg_cr \<and> can_chg_vr) (throwError IllegalOperation);
croot_cap' <- derive_cap (snd (excaps ! 0)) ((if ws ! Suc 0 = 0 then id else update_cap_data False (ws ! Suc 0)) (fst (excaps ! 0)));
y <- unlessE (is_cnode_cap croot_cap') (throwError IllegalOperation);
vroot_cap' <- derive_cap (snd (excaps ! Suc 0)) ((if ws ! 2 = 0 then id else update_cap_data False (ws ! 2)) (fst (excaps ! Suc 0)));
y <- unlessE (is_valid_vtable_root vroot_cap') (throwError IllegalOperation);
returnOk (ThreadControl t slot (Some (to_bl (ws ! 0))) None None (Some (croot_cap', snd (excaps ! 0))) (Some (vroot_cap', snd (excaps ! Suc 0))) None)
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>s. 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))) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<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); \<not> length ws < 3; \<not> length excaps < 2\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag ((if ws ! Suc 0 = 0 then \<lambda>a. a else update_cap_data False (ws ! Suc 0)) (fst (excaps ! 0))) \<and> is_subject aag (fst (snd (excaps ! 0))) \<and> pas_cap_cur_auth aag ((if ws ! 2 = 0 then \<lambda>a. a else update_cap_data False (ws ! 2)) (fst (excaps ! Suc 0))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag t; 3 \<le> length ws; 2 \<le> length excaps; is_subject aag (fst (snd (excaps ! 0))); is_subject aag (fst (snd (excaps ! Suc 0))); pas_cap_cur_auth aag (fst (excaps ! 0)); pas_cap_cur_auth aag (fst (excaps ! Suc 0))\<rbrakk> \<Longrightarrow> (ws ! 2 = 0 \<longrightarrow> ws ! Suc 0 \<noteq> 0 \<longrightarrow> pas_cap_cur_auth aag (update_cap_data False (ws ! Suc 0) (fst (excaps ! 0)))) \<and> (ws ! 2 \<noteq> 0 \<longrightarrow> (ws ! Suc 0 = 0 \<longrightarrow> pas_cap_cur_auth aag (update_cap_data False (ws ! 2) (fst (excaps ! Suc 0)))) \<and> (ws ! Suc 0 \<noteq> 0 \<longrightarrow> pas_cap_cur_auth aag (update_cap_data False (ws ! Suc 0) (fst (excaps ! 0))) \<and> pas_cap_cur_auth aag (update_cap_data False (ws ! 2) (fst (excaps ! Suc 0))))) proof (prove)
goal:
No subgoals!