theory Access_AC

lemma cdt_change_allowed_delete_derived:
  "\<lbrakk> valid_objs s; valid_mdb s; pas_refined aag s; cdt_change_allowed' aag slot s \<rbrakk>
     \<Longrightarrow> aag_has_auth_to aag DeleteDerived (fst slot)" apply (elim cdt_change_allowedE cdt_direct_change_allowed.cases) apply (erule rtrancl_induct) apply (solves\<open>simp add: pas_refined_refl\<close>) apply (fastforce simp: cdt_parent_of_def
                    dest: aag_cdt_link_DeleteDerived
                   intro: aag_wellformed_delete_derived_trans) apply (clarsimp simp: direct_call_def ep_recv_blocked_def) apply (frule(1)tcb_states_of_state_to_auth) apply (elim tcb_states_of_state_kheapE) apply (frule(2) descendant_of_caller_slot[OF _ _ tcb_atI]) apply (frule(1) parent_of_rtrancl_no_descendant) apply clarsimp by (rule aag_wellformed_delete_derived'[OF _ _ pas_refined_wellformed])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; cdt_change_allowed' aag slot s\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst slot)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>pptr. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; cdt s \<Turnstile> pptr \<rightarrow>* slot; pasObjectAbs aag (fst pptr) \<in> {pasSubject aag}\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst slot)) \<in> pasPolicy aag
 2. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; cdt s \<Turnstile> pptr \<rightarrow>* slot; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst slot)) \<in> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<And>pptr. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; pasObjectAbs aag (fst pptr) \<in> {pasSubject aag}\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst pptr)) \<in> pasPolicy aag
 2. \<And>pptr y z. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; pasObjectAbs aag (fst pptr) \<in> {pasSubject aag}; cdt s \<Turnstile> pptr \<rightarrow>* y; cdt s \<Turnstile> y \<leadsto> z; (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst y)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst z)) \<in> pasPolicy aag
 3. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; cdt s \<Turnstile> pptr \<rightarrow>* slot; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst slot)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>pptr y z. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; pasObjectAbs aag (fst pptr) \<in> {pasSubject aag}; cdt s \<Turnstile> pptr \<rightarrow>* y; cdt s \<Turnstile> y \<leadsto> z; (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst y)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst z)) \<in> pasPolicy aag
 2. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; cdt s \<Turnstile> pptr \<rightarrow>* slot; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst slot)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; cdt s \<Turnstile> pptr \<rightarrow>* slot; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst slot)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>a ep pl. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; cdt s \<Turnstile> (a, tcb_cnode_index 3) \<rightarrow>* slot; tcb_states_of_state s a = Some (BlockedOnReceive ep pl); (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst slot)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>a ep pl. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; cdt s \<Turnstile> (a, tcb_cnode_index 3) \<rightarrow>* slot; tcb_states_of_state s a = Some (BlockedOnReceive ep pl); (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; \<forall>(obj, auth)\<in>tcb_st_to_auth (BlockedOnReceive ep pl). (pasObjectAbs aag a, auth, pasObjectAbs aag obj) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst slot)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>a ep pl tcb. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; cdt s \<Turnstile> (a, tcb_cnode_index 3) \<rightarrow>* slot; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; \<forall>(obj, auth)\<in>tcb_st_to_auth (BlockedOnReceive ep pl). (pasObjectAbs aag a, auth, pasObjectAbs aag obj) \<in> pasPolicy aag; kheap s a = Some (TCB tcb); tcb_state tcb = BlockedOnReceive ep pl\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst slot)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>a ep pl tcb. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; cdt s \<Turnstile> (a, tcb_cnode_index 3) \<rightarrow>* slot; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; \<forall>(obj, auth)\<in>tcb_st_to_auth (BlockedOnReceive ep pl). (pasObjectAbs aag a, auth, pasObjectAbs aag obj) \<in> pasPolicy aag; kheap s a = Some (TCB tcb); tcb_state tcb = BlockedOnReceive ep pl; descendants_of (a, tcb_cnode_index 3) (cdt s) = {}\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst slot)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>a ep pl tcb. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; cdt s \<Turnstile> (a, tcb_cnode_index 3) \<rightarrow>* slot; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; \<forall>(obj, auth)\<in>tcb_st_to_auth (BlockedOnReceive ep pl). (pasObjectAbs aag a, auth, pasObjectAbs aag obj) \<in> pasPolicy aag; kheap s a = Some (TCB tcb); tcb_state tcb = BlockedOnReceive ep pl; descendants_of (a, tcb_cnode_index 3) (cdt s) = {}; (a, tcb_cnode_index 3) = slot\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag (fst slot)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>a ep pl tcb. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; kheap s a = Some (TCB tcb); tcb_state tcb = BlockedOnReceive ep pl; descendants_of (a, tcb_cnode_index 3) (cdt s) = {}; slot = (a, tcb_cnode_index 3); (pasObjectAbs aag a, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; \<forall>x\<in>if receiver_can_grant pl then {(ep, Grant)} else {}. case x of (obj, auth) \<Rightarrow> (pasObjectAbs aag a, auth, pasObjectAbs aag obj) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, DeleteDerived, pasObjectAbs aag a) \<in> pasPolicy aag