theory FinalCaps

lemma cdt_change_allowed_not_silc:
  "\<lbrakk> valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; cdt_change_allowed' aag ptr s \<rbrakk>
     \<Longrightarrow> pasObjectAbs aag (fst ptr) \<noteq> SilcLabel" 
  (* very manual *)
   apply (frule(3) cca_to_transferable_or_subject) apply (frule silc_inv_not_subject) apply (elim disjE; simp?) apply (intro notI) apply (rule silc_inv_no_transferable', assumption, assumption) apply (elim cdt_change_allowedE cdt_direct_change_allowed.cases) apply (clarsimp simp:rtrancl_eq_or_trancl, elim disjE, solves\<open>clarsimp\<close>) apply (clarsimp dest!: tranclD2 parent_ofD) apply (drule valid_mdb_mdb_cte_at) apply (drule(1) mdb_cte_atD[rotated],clarsimp simp: cte_wp_at_caps_of_state) apply (rule silc_inv_cnode_onlyE, assumption, assumption) apply (erule tcb_states_of_state_kheapE) apply (frule(2) descendant_of_caller_slot[OF _ _ tcb_atI]) apply clarsimp apply (frule(1) parent_of_rtrancl_no_descendant) apply (force simp add:is_cap_table obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; cdt_change_allowed' aag ptr s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (fst ptr) \<noteq> SilcLabel proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; cdt_change_allowed' aag ptr s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (fst ptr) \<noteq> SilcLabel proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; cdt_change_allowed' aag ptr s; is_subject aag (fst ptr) \<or> is_transferable_in ptr s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (fst ptr) \<noteq> SilcLabel proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; cdt_change_allowed' aag ptr s; is_subject aag (fst ptr) \<or> is_transferable_in ptr s; SilcLabel \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> pasObjectAbs aag (fst ptr) \<noteq> SilcLabel proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; cdt_change_allowed' aag ptr s; SilcLabel \<noteq> pasSubject aag; is_transferable_in ptr s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (fst ptr) \<noteq> SilcLabel proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; cdt_change_allowed' aag ptr s; SilcLabel \<noteq> pasSubject aag; is_transferable_in ptr s; pasObjectAbs aag (fst ptr) = SilcLabel\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; cdt_change_allowed' aag ptr s; SilcLabel \<noteq> pasSubject aag; is_transferable_in ptr s; pasObjectAbs aag (fst ptr) = SilcLabel\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) ptr s proof (prove)
goal (2 subgoals):
 1. \<And>pptr. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; SilcLabel \<noteq> pasSubject aag; is_transferable_in ptr s; pasObjectAbs aag (fst ptr) = SilcLabel; cdt s \<Turnstile> pptr \<rightarrow>* ptr; pasObjectAbs aag (fst pptr) \<in> {pasSubject aag}\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) ptr s
 2. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; SilcLabel \<noteq> pasSubject aag; is_transferable_in ptr s; pasObjectAbs aag (fst ptr) = SilcLabel; cdt s \<Turnstile> pptr \<rightarrow>* ptr; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) ptr s proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; SilcLabel \<noteq> pasSubject aag; is_transferable_in ptr s; pasObjectAbs aag (fst ptr) = SilcLabel; is_subject aag a; (a, b) \<noteq> ptr \<and> cdt s \<Turnstile> (a, b) \<rightarrow> ptr\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) ptr s
 2. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; SilcLabel \<noteq> pasSubject aag; is_transferable_in ptr s; pasObjectAbs aag (fst ptr) = SilcLabel; cdt s \<Turnstile> pptr \<rightarrow>* ptr; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) ptr s proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; SilcLabel \<noteq> pasSubject aag; is_transferable_in ptr s; pasObjectAbs aag (fst ptr) = SilcLabel; is_subject aag a; (a, b) \<noteq> ptr; cdt s \<Turnstile> (a, b) \<rightarrow>* (aa, ba); cdt s ptr = Some (aa, ba)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) ptr s
 2. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; SilcLabel \<noteq> pasSubject aag; is_transferable_in ptr s; pasObjectAbs aag (fst ptr) = SilcLabel; cdt s \<Turnstile> pptr \<rightarrow>* ptr; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) ptr s proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>valid_objs s; pas_refined aag s; silc_inv aag st s; SilcLabel \<noteq> pasSubject aag; is_transferable_in ptr s; pasObjectAbs aag (fst ptr) = SilcLabel; is_subject aag a; (a, b) \<noteq> ptr; cdt s \<Turnstile> (a, b) \<rightarrow>* (aa, ba); cdt s ptr = Some (aa, ba); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) ptr s
 2. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; SilcLabel \<noteq> pasSubject aag; is_transferable_in ptr s; pasObjectAbs aag (fst ptr) = SilcLabel; cdt s \<Turnstile> pptr \<rightarrow>* ptr; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; SilcLabel \<noteq> pasSubject aag; is_transferable_in ptr s; pasObjectAbs aag (fst ptr) = SilcLabel; cdt s \<Turnstile> pptr \<rightarrow>* ptr; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>pptr tcbst ep sz. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; SilcLabel \<noteq> pasSubject aag; is_transferable_in ptr s; pasObjectAbs aag (fst ptr) = SilcLabel; cdt s \<Turnstile> pptr \<rightarrow>* ptr; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3; cap_table_at sz (fst ptr) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>pptr tcbst ep sz tcb. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; SilcLabel \<noteq> pasSubject aag; is_transferable_in ptr s; pasObjectAbs aag (fst ptr) = SilcLabel; cdt s \<Turnstile> pptr \<rightarrow>* ptr; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3; cap_table_at sz (fst ptr) s; kheap s (fst pptr) = Some (TCB tcb); tcb_state tcb = tcbst\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>pptr tcbst ep sz tcb. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; SilcLabel \<noteq> pasSubject aag; is_transferable_in ptr s; pasObjectAbs aag (fst ptr) = SilcLabel; cdt s \<Turnstile> pptr \<rightarrow>* ptr; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3; cap_table_at sz (fst ptr) s; kheap s (fst pptr) = Some (TCB tcb); tcb_state tcb = tcbst; descendants_of (fst pptr, tcb_cnode_index 3) (cdt s) = {}\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>a ep sz tcb. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; SilcLabel \<noteq> pasSubject aag; is_transferable_in ptr s; pasObjectAbs aag (fst ptr) = SilcLabel; cdt s \<Turnstile> (a, tcb_cnode_index 3) \<rightarrow>* ptr; direct_call {pasSubject aag} aag ep (tcb_state tcb); cap_table_at sz (fst ptr) s; kheap s a = Some (TCB tcb); descendants_of (a, tcb_cnode_index 3) (cdt s) = {}\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>a ep sz tcb. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; silc_inv aag st s; SilcLabel \<noteq> pasSubject aag; is_transferable_in ptr s; pasObjectAbs aag (fst ptr) = SilcLabel; cdt s \<Turnstile> (a, tcb_cnode_index 3) \<rightarrow>* ptr; direct_call {pasSubject aag} aag ep (tcb_state tcb); cap_table_at sz (fst ptr) s; kheap s a = Some (TCB tcb); descendants_of (a, tcb_cnode_index 3) (cdt s) = {}; (a, tcb_cnode_index 3) = ptr\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) ptr s proof (prove)
goal:
No subgoals!