theory Tcb_AC

lemma decode_tcb_configure_authorised_helper:
  "\<lbrace>K True and 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))
                                   \<and> authorised_tcb_inv aag set_param
                                   \<and> is_ThreadControl set_param)\<rbrace>
   decode_set_space ws (ThreadCap t) slot excaps
   \<lbrace>\<lambda>rv _ :: det_ext state. authorised_tcb_inv aag (ThreadControl t slot (tc_new_fault_ep rv)
                                                                  None None (tc_new_croot rv)
                                                                  (tc_new_vroot rv)
                                                                  (tc_new_buffer set_param))\<rbrace>, -" apply (rule hoare_gen_asmE) apply (cases set_param) apply (simp_all add: decode_set_space_def authorised_tcb_inv_def
                 cong: list.case_cong option.case_cong prod.case_cong
                split: prod.split_asm split del: if_split) apply (cases "excaps!0") apply (cases "excaps!Suc 0") apply (rule hoare_pre) apply (clarsimp simp: ball_Un 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)+ apply (clarsimp cong: list.case_cong option.case_cong prod.case_cong split: prod.split_asm) 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 True and 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)) \<and> authorised_tcb_inv aag set_param \<and> is_ThreadControl set_param)\<rbrace> decode_set_space ws (ThreadCap t) slot excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag (ThreadControl t slot (tc_new_fault_ep rv) None None (tc_new_croot rv) (tc_new_vroot rv) (tc_new_buffer set_param))\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. 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)) \<and> authorised_tcb_inv aag set_param \<and> is_ThreadControl set_param \<Longrightarrow> \<lbrace>K True\<rbrace> decode_set_space ws (ThreadCap t) slot excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag (ThreadControl t slot (tc_new_fault_ep rv) None None (tc_new_croot rv) (tc_new_vroot rv) (tc_new_buffer set_param))\<rbrace>, - proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>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)) \<and> authorised_tcb_inv aag set_param \<and> is_ThreadControl set_param; set_param = WriteRegisters x11 x12 x13 x14\<rbrakk> \<Longrightarrow> \<lbrace>K True\<rbrace> decode_set_space ws (ThreadCap t) slot excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag (ThreadControl t slot (tc_new_fault_ep rv) None None (tc_new_croot rv) (tc_new_vroot rv) (tc_new_buffer set_param))\<rbrace>, -
 2. \<And>x21 x22 x23 x24. \<lbrakk>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)) \<and> authorised_tcb_inv aag set_param \<and> is_ThreadControl set_param; set_param = ReadRegisters x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>K True\<rbrace> decode_set_space ws (ThreadCap t) slot excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag (ThreadControl t slot (tc_new_fault_ep rv) None None (tc_new_croot rv) (tc_new_vroot rv) (tc_new_buffer set_param))\<rbrace>, -
 3. \<And>x31 x32 x33 x34 x35 x36 x37. \<lbrakk>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)) \<and> authorised_tcb_inv aag set_param \<and> is_ThreadControl set_param; set_param = CopyRegisters x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> \<lbrace>K True\<rbrace> decode_set_space ws (ThreadCap t) slot excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag (ThreadControl t slot (tc_new_fault_ep rv) None None (tc_new_croot rv) (tc_new_vroot rv) (tc_new_buffer set_param))\<rbrace>, -
 4. \<And>x41 x42 x43 x44 x45 x46 x47 x48. \<lbrakk>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)) \<and> authorised_tcb_inv aag set_param \<and> is_ThreadControl set_param; set_param = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48\<rbrakk> \<Longrightarrow> \<lbrace>K True\<rbrace> decode_set_space ws (ThreadCap t) slot excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag (ThreadControl t slot (tc_new_fault_ep rv) None None (tc_new_croot rv) (tc_new_vroot rv) (tc_new_buffer set_param))\<rbrace>, -
 5. \<And>x5. \<lbrakk>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)) \<and> authorised_tcb_inv aag set_param \<and> is_ThreadControl set_param; set_param = Suspend x5\<rbrakk> \<Longrightarrow> \<lbrace>K True\<rbrace> decode_set_space ws (ThreadCap t) slot excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag (ThreadControl t slot (tc_new_fault_ep rv) None None (tc_new_croot rv) (tc_new_vroot rv) (tc_new_buffer set_param))\<rbrace>, -
 6. \<And>x6. \<lbrakk>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)) \<and> authorised_tcb_inv aag set_param \<and> is_ThreadControl set_param; set_param = Resume x6\<rbrakk> \<Longrightarrow> \<lbrace>K True\<rbrace> decode_set_space ws (ThreadCap t) slot excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag (ThreadControl t slot (tc_new_fault_ep rv) None None (tc_new_croot rv) (tc_new_vroot rv) (tc_new_buffer set_param))\<rbrace>, -
 7. \<And>x71 x72. \<lbrakk>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)) \<and> authorised_tcb_inv aag set_param \<and> is_ThreadControl set_param; set_param = NotificationControl x71 x72\<rbrakk> \<Longrightarrow> \<lbrace>K True\<rbrace> decode_set_space ws (ThreadCap t) slot excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag (ThreadControl t slot (tc_new_fault_ep rv) None None (tc_new_croot rv) (tc_new_vroot rv) (tc_new_buffer set_param))\<rbrace>, -
 8. \<And>x81 x82. \<lbrakk>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)) \<and> authorised_tcb_inv aag set_param \<and> is_ThreadControl set_param; set_param = SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> \<lbrace>K True\<rbrace> decode_set_space ws (ThreadCap t) slot excaps \<lbrace>\<lambda>rv _. authorised_tcb_inv aag (ThreadControl t slot (tc_new_fault_ep rv) None None (tc_new_croot rv) (tc_new_vroot rv) (tc_new_buffer set_param))\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x44 x45 x46 x47 x48. \<lbrakk>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)) \<and> is_subject aag x41 \<and> (\<forall>(cap, slot)\<in>set_option x46 \<union> set_option x47 \<union> (case x48 of None \<Rightarrow> {} | Some x2 \<Rightarrow> set_option (snd x2)). pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)); set_param = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>y. True\<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 _. \<forall>x\<in>set_option (tc_new_croot rv) \<union> set_option (tc_new_vroot rv) \<union> (case x48 of None \<Rightarrow> {} | Some x2 \<Rightarrow> set_option (snd x2)). case x of (cap, slot) \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x44 x45 x46 x47 x48 a b c. \<lbrakk>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)) \<and> is_subject aag x41 \<and> (\<forall>(cap, slot)\<in>set_option x46 \<union> set_option x47 \<union> (case x48 of None \<Rightarrow> {} | Some x2 \<Rightarrow> set_option (snd x2)). pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)); set_param = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; excaps ! 0 = (a, b, c)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>y. True\<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 _. \<forall>x\<in>set_option (tc_new_croot rv) \<union> set_option (tc_new_vroot rv) \<union> (case x48 of None \<Rightarrow> {} | Some x2 \<Rightarrow> set_option (snd x2)). case x of (cap, slot) \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x44 x45 x46 x47 x48 a b c aa ba ca. \<lbrakk>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)) \<and> is_subject aag x41 \<and> (\<forall>(cap, slot)\<in>set_option x46 \<union> set_option x47 \<union> (case x48 of None \<Rightarrow> {} | Some x2 \<Rightarrow> set_option (snd x2)). pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)); set_param = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; excaps ! 0 = (a, b, c); excaps ! Suc 0 = (aa, ba, ca)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>y. True\<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 _. \<forall>x\<in>set_option (tc_new_croot rv) \<union> set_option (tc_new_vroot rv) \<union> (case x48 of None \<Rightarrow> {} | Some x2 \<Rightarrow> set_option (snd x2)). case x of (cap, slot) \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 x47 x48 a b c aa ba ca. \<lbrakk>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)) \<and> is_subject aag x41 \<and> (\<forall>(cap, slot)\<in>set_option x46 \<union> set_option x47 \<union> (case x48 of None \<Rightarrow> {} | Some x2 \<Rightarrow> set_option (snd x2)). pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)); set_param = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; excaps ! 0 = (a, b, c); excaps ! Suc 0 = (aa, ba, ca)\<rbrakk> \<Longrightarrow> \<lbrace>?P'32 x41 x42 x43 x44 x45 x46 x47 x48 a b c aa ba ca\<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 _. \<forall>x\<in>set_option (tc_new_croot rv) \<union> set_option (tc_new_vroot rv) \<union> (case x48 of None \<Rightarrow> {} | Some x2 \<Rightarrow> set_option (snd x2)). case x of (cap, slot) \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)\<rbrace>, -
 2. \<And>x41 x42 x43 x44 x45 x46 x47 x48 a b c aa ba ca s. \<lbrakk>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)) \<and> is_subject aag x41 \<and> (\<forall>(cap, slot)\<in>set_option x46 \<union> set_option x47 \<union> (case x48 of None \<Rightarrow> {} | Some x2 \<Rightarrow> set_option (snd x2)). pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)); set_param = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48; excaps ! 0 = (a, b, c); excaps ! Suc 0 = (aa, ba, ca); True\<rbrakk> \<Longrightarrow> ?P'32 x41 x42 x43 x44 x45 x46 x47 x48 a b c aa ba ca s proof (prove)
goal (1 subgoal):
 1. \<And>x41 a b x43 x44 x45 x46 x47 x48 aa ba c aaa baa ca. \<lbrakk>set_param = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48; excaps ! 0 = (aa, ba, c); excaps ! Suc 0 = (aaa, baa, ca); 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); is_subject aag x41; \<forall>x\<in>set_option x46. case x of (cap, slot) \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot); \<forall>x\<in>set_option x47. case x of (cap, slot) \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot); \<forall>x\<in>case x48 of None \<Rightarrow> {} | Some x2 \<Rightarrow> set_option (snd x2). case x of (cap, slot) \<Rightarrow> pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot); \<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)) aa) \<and> is_subject aag ba \<and> pas_cap_cur_auth aag ((if ws ! 2 = 0 then \<lambda>a. a else update_cap_data False (ws ! 2)) aaa) \<and> is_subject aag baa proof (prove)
goal (1 subgoal):
 1. \<And>x41 a b x43 x44 x45 x46 x47 x48 aa ba c aaa baa ca. \<lbrakk>\<forall>x\<in>case x48 of None \<Rightarrow> {} | Some x2 \<Rightarrow> set_option (snd x2). \<forall>x1 a. (\<forall>b. x \<noteq> (x1, a, b)) \<or> pas_cap_cur_auth aag x1 \<and> is_subject aag a; \<not> length ws < 3; \<not> length excaps < 2; set_param = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48; excaps ! 0 = (aa, ba, c); excaps ! Suc 0 = (aaa, baa, ca); 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); is_subject aag x41; \<forall>x\<in>set_option x46. \<forall>x1 a. (\<forall>b. x \<noteq> (x1, a, b)) \<or> pas_cap_cur_auth aag x1 \<and> is_subject aag a; \<forall>x\<in>set_option x47. \<forall>x1 a. (\<forall>b. x \<noteq> (x1, a, b)) \<or> pas_cap_cur_auth aag x1 \<and> is_subject aag a\<rbrakk> \<Longrightarrow> (ws ! 2 = 0 \<longrightarrow> (ws ! Suc 0 = 0 \<longrightarrow> pas_cap_cur_auth aag aa \<and> is_subject aag ba \<and> pas_cap_cur_auth aag aaa \<and> is_subject aag baa) \<and> (ws ! Suc 0 \<noteq> 0 \<longrightarrow> pas_cap_cur_auth aag (update_cap_data False (ws ! Suc 0) aa) \<and> is_subject aag ba \<and> pas_cap_cur_auth aag aaa \<and> is_subject aag baa)) \<and> (ws ! 2 \<noteq> 0 \<longrightarrow> (ws ! Suc 0 = 0 \<longrightarrow> pas_cap_cur_auth aag aa \<and> is_subject aag ba \<and> pas_cap_cur_auth aag (update_cap_data False (ws ! 2) aaa) \<and> is_subject aag baa) \<and> (ws ! Suc 0 \<noteq> 0 \<longrightarrow> pas_cap_cur_auth aag (update_cap_data False (ws ! Suc 0) aa) \<and> is_subject aag ba \<and> pas_cap_cur_auth aag (update_cap_data False (ws ! 2) aaa) \<and> is_subject aag baa)) proof (prove)
goal (1 subgoal):
 1. \<And>x41 a b x43 x44 x45 x46 x47 x48 aa ba c aaa baa ca. \<lbrakk>\<forall>x\<in>case x48 of None \<Rightarrow> {} | Some x2 \<Rightarrow> set_option (snd x2). \<forall>x1 a. (\<forall>b. x \<noteq> (x1, a, b)) \<or> pas_cap_cur_auth aag x1 \<and> is_subject aag a; 3 \<le> length ws; 2 \<le> length excaps; set_param = ThreadControl x41 (a, b) x43 x44 x45 x46 x47 x48; excaps ! 0 = (aa, ba, c); excaps ! Suc 0 = (aaa, baa, ca); is_subject aag t; is_subject aag x41; \<forall>x\<in>set_option x46. \<forall>x1 a. (\<forall>b. x \<noteq> (x1, a, b)) \<or> pas_cap_cur_auth aag x1 \<and> is_subject aag a; \<forall>x\<in>set_option x47. \<forall>x1 a. (\<forall>b. x \<noteq> (x1, a, b)) \<or> pas_cap_cur_auth aag x1 \<and> is_subject aag a; is_subject aag ba; is_subject aag baa; pas_cap_cur_auth aag aa; pas_cap_cur_auth aag aaa\<rbrakk> \<Longrightarrow> (ws ! 2 = 0 \<longrightarrow> ws ! Suc 0 \<noteq> 0 \<longrightarrow> pas_cap_cur_auth aag (update_cap_data False (ws ! Suc 0) aa)) \<and> (ws ! 2 \<noteq> 0 \<longrightarrow> (ws ! Suc 0 = 0 \<longrightarrow> pas_cap_cur_auth aag (update_cap_data False (ws ! 2) aaa)) \<and> (ws ! Suc 0 \<noteq> 0 \<longrightarrow> pas_cap_cur_auth aag (update_cap_data False (ws ! Suc 0) aa) \<and> pas_cap_cur_auth aag (update_cap_data False (ws ! 2) aaa))) proof (prove)
goal:
No subgoals!