theory Access_AC

lemma tcb_caller_slot_empty_on_recieve:
  "\<lbrakk> valid_mdb s; valid_objs s; kheap s tcb_ptr = Some (TCB tcb); ep_recv_blocked ep (tcb_state tcb) \<rbrakk>
     \<Longrightarrow> tcb_caller tcb = NullCap \<and> cdt s (tcb_ptr,(tcb_cnode_index 3)) = None \<and>
         descendants_of (tcb_ptr,(tcb_cnode_index 3)) (cdt s) = {}" apply (simp only:valid_objs_def) apply (drule bspec,fastforce) apply (simp add:valid_obj_def) apply (simp only:valid_tcb_def) apply (drule conjunct1) apply (drule_tac x="the (tcb_cap_cases (tcb_cnode_index 3))" in  bspec) apply (fastforce simp:tcb_cap_cases_def) apply (simp add:tcb_cap_cases_def split: thread_state.splits) apply (subgoal_tac "caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap") apply (simp only: valid_mdb_def2, drule conjunct1) apply (intro conjI) apply (simp add: mdb_cte_at_def) apply (rule classical) apply fastforce apply (rule mdb_cte_at_no_descendants, fastforce+)[1] apply (fastforce simp add: tcb_cnode_map_def caps_of_state_tcb_index_trans[OF get_tcb_rev]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_objs s; kheap s tcb_ptr = Some (TCB tcb); ep_recv_blocked ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> tcb_caller tcb = NullCap \<and> cdt s (tcb_ptr, tcb_cnode_index 3) = None \<and> descendants_of (tcb_ptr, tcb_cnode_index 3) (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; \<forall>ptr\<in>dom $ kheap s. \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; kheap s tcb_ptr = Some (TCB tcb); ep_recv_blocked ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> tcb_caller tcb = NullCap \<and> cdt s (tcb_ptr, tcb_cnode_index 3) = None \<and> descendants_of (tcb_ptr, tcb_cnode_index 3) (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; kheap s tcb_ptr = Some (TCB tcb); ep_recv_blocked ep (tcb_state tcb); \<exists>obj. kheap s tcb_ptr = Some obj \<and> valid_obj tcb_ptr obj s\<rbrakk> \<Longrightarrow> tcb_caller tcb = NullCap \<and> cdt s (tcb_ptr, tcb_cnode_index 3) = None \<and> descendants_of (tcb_ptr, tcb_cnode_index 3) (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; kheap s tcb_ptr = Some (TCB tcb); ep_recv_blocked ep (tcb_state tcb); valid_tcb tcb_ptr tcb s\<rbrakk> \<Longrightarrow> tcb_caller tcb = NullCap \<and> cdt s (tcb_ptr, tcb_cnode_index 3) = None \<and> descendants_of (tcb_ptr, tcb_cnode_index 3) (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; kheap s tcb_ptr = Some (TCB tcb); ep_recv_blocked ep (tcb_state tcb); (\<forall>(getF, setF, restr)\<in>ran tcb_cap_cases. s \<turnstile> getF tcb \<and> restr tcb_ptr (tcb_state tcb) (getF tcb)) \<and> valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb) \<and> valid_tcb_state (tcb_state tcb) s \<and> (case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f) \<and> length (tcb_fault_handler tcb) = word_bits \<and> valid_bound_ntfn (tcb_bound_notification tcb) s \<and> valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> tcb_caller tcb = NullCap \<and> cdt s (tcb_ptr, tcb_cnode_index 3) = None \<and> descendants_of (tcb_ptr, tcb_cnode_index 3) (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; kheap s tcb_ptr = Some (TCB tcb); ep_recv_blocked ep (tcb_state tcb); \<forall>(getF, setF, restr)\<in>ran tcb_cap_cases. s \<turnstile> getF tcb \<and> restr tcb_ptr (tcb_state tcb) (getF tcb)\<rbrakk> \<Longrightarrow> tcb_caller tcb = NullCap \<and> cdt s (tcb_ptr, tcb_cnode_index 3) = None \<and> descendants_of (tcb_ptr, tcb_cnode_index 3) (cdt s) = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_mdb s; kheap s tcb_ptr = Some (TCB tcb); ep_recv_blocked ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> the (tcb_cap_cases (tcb_cnode_index 3)) \<in> ran tcb_cap_cases
 2. \<lbrakk>valid_mdb s; kheap s tcb_ptr = Some (TCB tcb); ep_recv_blocked ep (tcb_state tcb); case the (tcb_cap_cases (tcb_cnode_index 3)) of (getF, setF, restr) \<Rightarrow> s \<turnstile> getF tcb \<and> restr tcb_ptr (tcb_state tcb) (getF tcb)\<rbrakk> \<Longrightarrow> tcb_caller tcb = NullCap \<and> cdt s (tcb_ptr, tcb_cnode_index 3) = None \<and> descendants_of (tcb_ptr, tcb_cnode_index 3) (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; kheap s tcb_ptr = Some (TCB tcb); ep_recv_blocked ep (tcb_state tcb); case the (tcb_cap_cases (tcb_cnode_index 3)) of (getF, setF, restr) \<Rightarrow> s \<turnstile> getF tcb \<and> restr tcb_ptr (tcb_state tcb) (getF tcb)\<rbrakk> \<Longrightarrow> tcb_caller tcb = NullCap \<and> cdt s (tcb_ptr, tcb_cnode_index 3) = None \<and> descendants_of (tcb_ptr, tcb_cnode_index 3) (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42. \<lbrakk>valid_mdb s; kheap s tcb_ptr = Some (TCB tcb); NullCap = tcb_caller tcb; tcb_state tcb = BlockedOnReceive ep x42; x41 = ep\<rbrakk> \<Longrightarrow> cdt s (tcb_ptr, tcb_cnode_index 3) = None \<and> descendants_of (tcb_ptr, tcb_cnode_index 3) (cdt s) = {} proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42. \<lbrakk>valid_mdb s; kheap s tcb_ptr = Some (TCB tcb); NullCap = tcb_caller tcb; tcb_state tcb = BlockedOnReceive ep x42; x41 = ep; caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap\<rbrakk> \<Longrightarrow> cdt s (tcb_ptr, tcb_cnode_index 3) = None \<and> descendants_of (tcb_ptr, tcb_cnode_index 3) (cdt s) = {}
 2. \<And>x41 x42. \<lbrakk>valid_mdb s; kheap s tcb_ptr = Some (TCB tcb); NullCap = tcb_caller tcb; tcb_state tcb = BlockedOnReceive ep x42; x41 = ep\<rbrakk> \<Longrightarrow> caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42. \<lbrakk>kheap s tcb_ptr = Some (TCB tcb); NullCap = tcb_caller tcb; tcb_state tcb = BlockedOnReceive ep x42; x41 = ep; caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s)\<rbrakk> \<Longrightarrow> cdt s (tcb_ptr, tcb_cnode_index 3) = None \<and> descendants_of (tcb_ptr, tcb_cnode_index 3) (cdt s) = {}
 2. \<And>x41 x42. \<lbrakk>valid_mdb s; kheap s tcb_ptr = Some (TCB tcb); NullCap = tcb_caller tcb; tcb_state tcb = BlockedOnReceive ep x42; x41 = ep\<rbrakk> \<Longrightarrow> caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap proof (prove)
goal (3 subgoals):
 1. \<And>x41 x42. \<lbrakk>kheap s tcb_ptr = Some (TCB tcb); NullCap = tcb_caller tcb; tcb_state tcb = BlockedOnReceive ep x42; x41 = ep; caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s)\<rbrakk> \<Longrightarrow> cdt s (tcb_ptr, tcb_cnode_index 3) = None
 2. \<And>x41 x42. \<lbrakk>kheap s tcb_ptr = Some (TCB tcb); NullCap = tcb_caller tcb; tcb_state tcb = BlockedOnReceive ep x42; x41 = ep; caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s)\<rbrakk> \<Longrightarrow> descendants_of (tcb_ptr, tcb_cnode_index 3) (cdt s) = {}
 3. \<And>x41 x42. \<lbrakk>valid_mdb s; kheap s tcb_ptr = Some (TCB tcb); NullCap = tcb_caller tcb; tcb_state tcb = BlockedOnReceive ep x42; x41 = ep\<rbrakk> \<Longrightarrow> caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap proof (prove)
goal (3 subgoals):
 1. \<And>x41 x42. \<lbrakk>kheap s tcb_ptr = Some (TCB tcb); NullCap = tcb_caller tcb; tcb_state tcb = BlockedOnReceive ep x42; x41 = ep; caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap; \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. caps_of_state s (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (aa, ba) = Some c \<and> NullCap \<noteq> c)\<rbrakk> \<Longrightarrow> cdt s (tcb_ptr, tcb_cnode_index 3) = None
 2. \<And>x41 x42. \<lbrakk>kheap s tcb_ptr = Some (TCB tcb); NullCap = tcb_caller tcb; tcb_state tcb = BlockedOnReceive ep x42; x41 = ep; caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s)\<rbrakk> \<Longrightarrow> descendants_of (tcb_ptr, tcb_cnode_index 3) (cdt s) = {}
 3. \<And>x41 x42. \<lbrakk>valid_mdb s; kheap s tcb_ptr = Some (TCB tcb); NullCap = tcb_caller tcb; tcb_state tcb = BlockedOnReceive ep x42; x41 = ep\<rbrakk> \<Longrightarrow> caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap proof (prove)
goal (3 subgoals):
 1. \<And>x41 x42. \<lbrakk>kheap s tcb_ptr = Some (TCB tcb); NullCap = tcb_caller tcb; tcb_state tcb = BlockedOnReceive ep x42; x41 = ep; caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap; \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. caps_of_state s (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (aa, ba) = Some c \<and> NullCap \<noteq> c); cdt s (tcb_ptr, tcb_cnode_index 3) \<noteq> None\<rbrakk> \<Longrightarrow> cdt s (tcb_ptr, tcb_cnode_index 3) = None
 2. \<And>x41 x42. \<lbrakk>kheap s tcb_ptr = Some (TCB tcb); NullCap = tcb_caller tcb; tcb_state tcb = BlockedOnReceive ep x42; x41 = ep; caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s)\<rbrakk> \<Longrightarrow> descendants_of (tcb_ptr, tcb_cnode_index 3) (cdt s) = {}
 3. \<And>x41 x42. \<lbrakk>valid_mdb s; kheap s tcb_ptr = Some (TCB tcb); NullCap = tcb_caller tcb; tcb_state tcb = BlockedOnReceive ep x42; x41 = ep\<rbrakk> \<Longrightarrow> caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42. \<lbrakk>kheap s tcb_ptr = Some (TCB tcb); NullCap = tcb_caller tcb; tcb_state tcb = BlockedOnReceive ep x42; x41 = ep; caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s)\<rbrakk> \<Longrightarrow> descendants_of (tcb_ptr, tcb_cnode_index 3) (cdt s) = {}
 2. \<And>x41 x42. \<lbrakk>valid_mdb s; kheap s tcb_ptr = Some (TCB tcb); NullCap = tcb_caller tcb; tcb_state tcb = BlockedOnReceive ep x42; x41 = ep\<rbrakk> \<Longrightarrow> caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42. \<lbrakk>valid_mdb s; kheap s tcb_ptr = Some (TCB tcb); NullCap = tcb_caller tcb; tcb_state tcb = BlockedOnReceive ep x42; x41 = ep\<rbrakk> \<Longrightarrow> caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap proof (prove)
goal:
No subgoals!