theory Ipc_AI

lemma ep_queue_cap_to:
  "\<lbrakk> ko_at (Endpoint ep) p s; invs s;
     \<lbrakk> live (Endpoint ep) \<longrightarrow> queue_of ep \<noteq> [] \<rbrakk>
        \<Longrightarrow> t \<in> set (queue_of ep) \<rbrakk>
     \<Longrightarrow> ex_nonz_cap_to t s" apply (frule sym_refs_ko_atD, fastforce) apply (erule obj_at_valid_objsE, fastforce) apply (clarsimp simp: valid_obj_def) apply (cases ep, simp_all add: queue_of_def valid_ep_def live_def
                                 st_tcb_at_refs_of_rev) apply (drule(1) bspec) apply (erule st_tcb_ex_cap, clarsimp+) apply (drule(1) bspec) apply (erule st_tcb_ex_cap, clarsimp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (Endpoint ep) p s; invs s; live (Endpoint ep) \<longrightarrow> queue_of ep \<noteq> [] \<Longrightarrow> t \<in> set (queue_of ep)\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (Endpoint ep) p s; invs s; live (Endpoint ep) \<longrightarrow> queue_of ep \<noteq> [] \<Longrightarrow> t \<in> set (queue_of ep); state_refs_of s p = refs_of (Endpoint ep) \<and> (\<forall>(x, tp)\<in>refs_of (Endpoint ep). obj_at (\<lambda>ko. (p, symreftype tp) \<in> refs_of ko) x s)\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>invs s; live (Endpoint ep) \<longrightarrow> queue_of ep \<noteq> [] \<Longrightarrow> t \<in> set (queue_of ep); state_refs_of s p = refs_of (Endpoint ep) \<and> (\<forall>(x, tp)\<in>refs_of (Endpoint ep). obj_at (\<lambda>ko. (p, symreftype tp) \<in> refs_of ko) x s); kheap s p = Some ko; Endpoint ep = ko; valid_obj p ko s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; live (Endpoint ep) \<longrightarrow> queue_of ep \<noteq> [] \<Longrightarrow> t \<in> set (queue_of ep); kheap s p = Some (Endpoint ep); valid_ep ep s; state_refs_of s p = ep_q_refs_of ep; \<forall>x\<in>ep_q_refs_of ep. case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (p, symreftype tp) \<in> refs_of ko) x s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>invs s; t \<in> set x2; kheap s p = Some (Endpoint (SendEP x2)); x2 \<noteq> [] \<and> (\<forall>t\<in>set x2. tcb_at t s) \<and> distinct x2; state_refs_of s p = set x2 \<times> {EPSend}; \<forall>x\<in>set x2. st_tcb_at (\<lambda>ts. \<exists>pl. ts = BlockedOnSend p pl) x s; ep = SendEP x2\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s
 2. \<And>x3. \<lbrakk>invs s; t \<in> set x3; kheap s p = Some (Endpoint (RecvEP x3)); x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. tcb_at t s) \<and> distinct x3; state_refs_of s p = set x3 \<times> {EPRecv}; \<forall>x\<in>set x3. st_tcb_at (\<lambda>ts. \<exists>pl. ts = BlockedOnReceive p pl) x s; ep = RecvEP x3\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>invs s; t \<in> set x2; kheap s p = Some (Endpoint (SendEP x2)); x2 \<noteq> [] \<and> (\<forall>t\<in>set x2. tcb_at t s) \<and> distinct x2; state_refs_of s p = set x2 \<times> {EPSend}; ep = SendEP x2; st_tcb_at (\<lambda>ts. \<exists>pl. ts = BlockedOnSend p pl) t s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s
 2. \<And>x3. \<lbrakk>invs s; t \<in> set x3; kheap s p = Some (Endpoint (RecvEP x3)); x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. tcb_at t s) \<and> distinct x3; state_refs_of s p = set x3 \<times> {EPRecv}; \<forall>x\<in>set x3. st_tcb_at (\<lambda>ts. \<exists>pl. ts = BlockedOnReceive p pl) x s; ep = RecvEP x3\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>invs s; t \<in> set x3; kheap s p = Some (Endpoint (RecvEP x3)); state_refs_of s p = set x3 \<times> {EPRecv}; \<forall>x\<in>set x3. st_tcb_at (\<lambda>ts. \<exists>pl. ts = BlockedOnReceive p pl) x s; ep = RecvEP x3; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at t s; distinct x3\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>invs s; t \<in> set x3; kheap s p = Some (Endpoint (RecvEP x3)); state_refs_of s p = set x3 \<times> {EPRecv}; ep = RecvEP x3; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at t s; distinct x3; st_tcb_at (\<lambda>ts. \<exists>pl. ts = BlockedOnReceive p pl) t s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s proof (prove)
goal:
No subgoals!