kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_AC

lemma lookup_cap_and_slot_authorised:
  "\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace>
   lookup_cap_and_slot thread xs
   \<lbrace>\<lambda>rv _. is_subject aag (fst (snd rv))\<rbrace>, -" unfolding lookup_cap_and_slot_def by (wp lookup_slot_for_thread_authorised | simp add: split_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace> lookup_cap_and_slot thread xs \<lbrace>\<lambda>rv _. is_subject aag (fst (snd rv))\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace> doE (slot, cr) <- lookup_slot_for_thread thread xs;
cap <- liftE $ get_cap slot;
returnOk (cap, slot)
odE \<lbrace>\<lambda>rv _. is_subject aag (fst (snd rv))\<rbrace>, -
theory Ipc_AC

lemma lookup_extra_caps_authorised:
  "\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace>
   lookup_extra_caps thread buffer mi
   \<lbrace>\<lambda>rv _. \<forall>cap \<in> set rv. is_subject aag (fst (snd cap))\<rbrace>, -" unfolding lookup_extra_caps_def by (wpsimp wp: mapME_set lookup_cap_and_slot_authorised)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace> lookup_extra_caps thread buffer mi \<lbrace>\<lambda>rv _. \<forall>cap\<in>set rv. is_subject aag (fst (snd cap))\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace> (liftE $ get_extra_cptrs buffer mi) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False $ lookup_cap_and_slot thread cptr) \<lbrace>\<lambda>rv _. \<forall>cap\<in>set rv. is_subject aag (fst (snd cap))\<rbrace>, -
theory Ipc_AC

lemma lookup_cap_and_slot_cur_auth:
   "\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace>
    lookup_cap_and_slot thread xs
    \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>, -" unfolding lookup_cap_and_slot_def by (wp get_cap_auth_wp [where aag = aag] lookup_slot_for_thread_authorised | simp add: split_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace> lookup_cap_and_slot thread xs \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace> doE (slot, cr) <- lookup_slot_for_thread thread xs;
cap <- liftE $ get_cap slot;
returnOk (cap, slot)
odE \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>, -
theory Ipc_AC

lemma lookup_extra_caps_auth:
  "\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace>
   lookup_extra_caps thread buffer mi
   \<lbrace>\<lambda>rv _. \<forall>cap \<in> set rv. pas_cap_cur_auth aag (fst cap)\<rbrace>, -" unfolding lookup_extra_caps_def by (wpsimp wp: mapME_set lookup_cap_and_slot_cur_auth)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace> lookup_extra_caps thread buffer mi \<lbrace>\<lambda>rv _. \<forall>cap\<in>set rv. pas_cap_cur_auth aag (fst cap)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace> (liftE $ get_extra_cptrs buffer mi) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False $ lookup_cap_and_slot thread cptr) \<lbrace>\<lambda>rv _. \<forall>cap\<in>set rv. pas_cap_cur_auth aag (fst cap)\<rbrace>, -
theory Ipc_AC

lemma transfer_caps_empty_inv:
  "transfer_caps mi [] endpoint receiver rbuf \<lbrace>P\<rbrace>" unfolding transfer_caps_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> transfer_caps mi [] endpoint receiver rbuf \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do dest_slots <- get_receive_slots receiver rbuf;
mi' <- return $ MI (mi_length mi) 0 0 (mi_label mi);
case rbuf of None \<Rightarrow> return mi' | Some receive_buffer \<Rightarrow> transfer_caps_loop endpoint receive_buffer 0 [] dest_slots mi'
od \<lbrace>\<lambda>_. P\<rbrace>
theory Ipc_AC

lemma lcs_valid':
  "\<lbrace>valid_objs\<rbrace> lookup_cap_and_slot thread xs \<lbrace>\<lambda>x s. s \<turnstile> fst x\<rbrace>, -" unfolding lookup_cap_and_slot_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> lookup_cap_and_slot thread xs \<lbrace>\<lambda>x s. s \<turnstile> fst x\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> doE (slot, cr) <- lookup_slot_for_thread thread xs;
cap <- liftE $ get_cap slot;
returnOk (cap, slot)
odE \<lbrace>\<lambda>x s. s \<turnstile> fst x\<rbrace>, -
theory Ipc_AC

lemma hoare_conjDR1:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> R rv s\<rbrace>, - \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -" by (simp add:validE_def validE_R_def valid_def) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> R rv s\<rbrace>, - \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -
theory Ipc_AC

lemma hoare_conjDR2:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> R rv s\<rbrace>, - \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, -" by (simp add:validE_def validE_R_def valid_def) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> R rv s\<rbrace>, - \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, -
theory Ipc_AC

lemma do_ipc_transfer_pas_refined:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
                    and valid_objs and valid_mdb
                    and K (grant \<longrightarrow> is_subject aag sender)
                    and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace>
   do_ipc_transfer sender ep badge grant receiver
   \<lbrace>\<lambda>_ s :: det_ext state. pas_refined aag s\<rbrace>" unfolding do_ipc_transfer_def by (wpsimp wp: do_normal_transfer_pas_refined hoare_vcg_all_lift hoare_drop_imps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace> do_ipc_transfer sender ep badge grant receiver \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)\<rbrace> do recv_buffer <- lookup_ipc_buffer True receiver;
fault <- thread_get tcb_fault sender;
case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False sender;
do_normal_transfer sender send_buffer ep badge grant receiver recv_buffer
od | Some f \<Rightarrow> do_fault_transfer badge sender receiver recv_buffer
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory Ipc_AC

lemma sym_ref_endpoint_recvD:
  assumes sym: "sym_refs (state_refs_of s)"
  and ep: "ko_at (Endpoint (RecvEP l)) epptr s"
  and inl: "t \<in> set l"
  shows "\<exists>pl. st_tcb_at ((=) (BlockedOnReceive epptr pl)) t s" proof - have "(t, EPRecv) \<in> state_refs_of s epptr" using ep inl by (force simp: state_refs_of_def dest:ko_atD) hence "(epptr, TCBBlockedRecv) \<in> state_refs_of s t" using sym by (force dest:sym_refsD[rotated]) thus ?thesis by (force simp: st_tcb_at_tcb_states_of_state_eq tcb_states_of_state_def get_tcb_def
                    state_refs_of_def tcb_st_refs_of_def tcb_bound_refs_def ep_q_refs_of_def
                    ntfn_q_refs_of_def ntfn_bound_refs_def
             split: ntfn.splits endpoint.splits thread_state.splits option.splits
                    kernel_object.splits) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>pl. st_tcb_at ((=) (BlockedOnReceive epptr pl)) t s proof (state)
goal (1 subgoal):
 1. \<exists>pl. st_tcb_at ((=) (BlockedOnReceive epptr pl)) t s proof (prove)
goal (1 subgoal):
 1. (t, EPRecv) \<in> state_refs_of s epptr proof (prove)
using this:
ko_at (Endpoint (RecvEP l)) epptr s
t \<in> set l

goal (1 subgoal):
 1. (t, EPRecv) \<in> state_refs_of s epptr proof (state)
this:
(t, EPRecv) \<in> state_refs_of s epptr

goal (1 subgoal):
 1. \<exists>pl. st_tcb_at ((=) (BlockedOnReceive epptr pl)) t s proof (prove)
using this:
(t, EPRecv) \<in> state_refs_of s epptr

goal (1 subgoal):
 1. (epptr, TCBBlockedRecv) \<in> state_refs_of s t proof (prove)
using this:
(t, EPRecv) \<in> state_refs_of s epptr
sym_refs (state_refs_of s)

goal (1 subgoal):
 1. (epptr, TCBBlockedRecv) \<in> state_refs_of s t proof (state)
this:
(epptr, TCBBlockedRecv) \<in> state_refs_of s t

goal (1 subgoal):
 1. \<exists>pl. st_tcb_at ((=) (BlockedOnReceive epptr pl)) t s proof (prove)
using this:
(epptr, TCBBlockedRecv) \<in> state_refs_of s t

goal (1 subgoal):
 1. \<exists>pl. st_tcb_at ((=) (BlockedOnReceive epptr pl)) t s proof (state)
this:
\<exists>pl. st_tcb_at ((=) (BlockedOnReceive epptr pl)) t s

goal:
No subgoals!
theory Ipc_AC

lemma send_ipc_valid_ep_helper:
  "\<lbrakk> invs s; ko_at (Endpoint (RecvEP (h # t))) epptr s \<rbrakk>
     \<Longrightarrow> valid_ep (case t of [] \<Rightarrow> IdleEP | h' # t'  \<Rightarrow> RecvEP t) s" apply (drule invs_valid_objs) apply (drule ko_atD) apply (erule(1) valid_objsE) by (cases t; simp add: valid_obj_def valid_ep_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; ko_at (Endpoint (RecvEP (h # t))) epptr s\<rbrakk> \<Longrightarrow> valid_ep (case t of [] \<Rightarrow> IdleEP | h' # t' \<Rightarrow> RecvEP t) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (Endpoint (RecvEP (h # t))) epptr s; valid_objs s\<rbrakk> \<Longrightarrow> valid_ep (case t of [] \<Rightarrow> IdleEP | h' # t' \<Rightarrow> RecvEP t) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; kheap s epptr = Some (Endpoint (RecvEP (h # t)))\<rbrakk> \<Longrightarrow> valid_ep (case t of [] \<Rightarrow> IdleEP | h' # t' \<Rightarrow> RecvEP t) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s epptr = Some (Endpoint (RecvEP (h # t))); valid_obj epptr (Endpoint (RecvEP (h # t))) s\<rbrakk> \<Longrightarrow> valid_ep (case t of [] \<Rightarrow> IdleEP | h' # t' \<Rightarrow> RecvEP t) s
theory Ipc_AC

lemma set_simple_ko_get_tcb:
  "set_simple_ko f ep epptr \<lbrace>\<lambda>s. P (get_tcb p s)\<rbrace>" unfolding set_simple_ko_def set_object_def apply (wp get_object_wp) apply (auto simp: partial_inv_def a_type_def get_tcb_def obj_at_def the_equality
             split: kernel_object.splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (get_tcb p s)\<rbrace> set_simple_ko f ep epptr \<lbrace>\<lambda>_ s. P (get_tcb p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (get_tcb p s)\<rbrace> do obj <- get_object ep;
assert (is_simple_type obj);
assert (partial_inv f obj \<noteq> None);
kobj <- get_object ep;
assert (a_type kobj = a_type (f epptr));
s <- get;
put (s\<lparr>kheap := (kheap s)(ep \<mapsto> f epptr)\<rparr>)
od \<lbrace>\<lambda>_ s. P (get_tcb p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (get_tcb p s) \<Longrightarrow> \<forall>ko. ko_at ko ep s \<longrightarrow> is_simple_type ko \<longrightarrow> partial_inv f ko \<noteq> None \<longrightarrow> (\<forall>ko. ko_at ko ep s \<longrightarrow> a_type ko = a_type (f epptr) \<longrightarrow> P (get_tcb p (s\<lparr>kheap := (kheap s)(ep \<mapsto> f epptr)\<rparr>))) proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma complete_signal_integrity:
  "\<lbrace>integrity aag X st and pas_refined aag and valid_objs
                       and bound_tcb_at ((=) (Some ntfnptr)) thread
                       and K (is_subject aag thread)\<rbrace>
   complete_signal ntfnptr thread
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: complete_signal_def) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (wpsimp wp: set_notification_respects[where auth=Receive]
                    set_thread_state_integrity_autarch as_user_integrity_autarch) apply (drule_tac t="pasSubject aag" in sym) apply (fastforce intro!: bound_tcb_at_implies_receive) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and valid_objs and bound_tcb_at ((=) (Some ntfnptr)) thread and K (is_subject aag thread)\<rbrace> complete_signal ntfnptr thread \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and valid_objs and bound_tcb_at ((=) (Some ntfnptr)) thread and (\<lambda>y. is_subject aag thread)\<rbrace> do ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn
od | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and bound_tcb_at ((=) (Some ntfnptr)) thread and (\<lambda>y. is_subject aag thread))\<rbrace> case ntfn_obj ntfn of ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn
od | _ \<Rightarrow> fail \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; integrity aag X st s; pas_refined aag s; valid_objs s; bound_tcb_at ((=) (Some ntfnptr)) thread s; is_subject aag thread; ntfn_obj ntfn = ActiveNtfn x\<rbrakk> \<Longrightarrow> (pasSubject aag, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; integrity aag X st s; pas_refined aag s; valid_objs s; bound_tcb_at ((=) (Some ntfnptr)) thread s; ntfn_obj ntfn = ActiveNtfn x; pasSubject aag = pasObjectAbs aag thread\<rbrakk> \<Longrightarrow> (pasSubject aag, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma sym_ref_endpoint_sendD:
  assumes sym: "sym_refs (state_refs_of s)"
  and ep: "ko_at (Endpoint (SendEP l)) epptr s"
  and inl: "t \<in> set l"
  shows "\<exists>pl. st_tcb_at ((=) (BlockedOnSend epptr pl)) t s" proof - have "(t, EPSend) \<in> state_refs_of s epptr" using ep inl by (force simp: state_refs_of_def dest:ko_atD) hence "(epptr, TCBBlockedSend) \<in> state_refs_of s t" using sym by (force dest:sym_refsD[rotated]) thus ?thesis by (force simp: st_tcb_at_tcb_states_of_state_eq tcb_states_of_state_def get_tcb_def
                    state_refs_of_def tcb_st_refs_of_def tcb_bound_refs_def ep_q_refs_of_def
                    ntfn_q_refs_of_def ntfn_bound_refs_def
             split: ntfn.splits endpoint.splits thread_state.splits option.splits
                    kernel_object.splits) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>pl. st_tcb_at ((=) (BlockedOnSend epptr pl)) t s proof (state)
goal (1 subgoal):
 1. \<exists>pl. st_tcb_at ((=) (BlockedOnSend epptr pl)) t s proof (prove)
goal (1 subgoal):
 1. (t, EPSend) \<in> state_refs_of s epptr proof (prove)
using this:
ko_at (Endpoint (SendEP l)) epptr s
t \<in> set l

goal (1 subgoal):
 1. (t, EPSend) \<in> state_refs_of s epptr proof (state)
this:
(t, EPSend) \<in> state_refs_of s epptr

goal (1 subgoal):
 1. \<exists>pl. st_tcb_at ((=) (BlockedOnSend epptr pl)) t s proof (prove)
using this:
(t, EPSend) \<in> state_refs_of s epptr

goal (1 subgoal):
 1. (epptr, TCBBlockedSend) \<in> state_refs_of s t proof (prove)
using this:
(t, EPSend) \<in> state_refs_of s epptr
sym_refs (state_refs_of s)

goal (1 subgoal):
 1. (epptr, TCBBlockedSend) \<in> state_refs_of s t proof (state)
this:
(epptr, TCBBlockedSend) \<in> state_refs_of s t

goal (1 subgoal):
 1. \<exists>pl. st_tcb_at ((=) (BlockedOnSend epptr pl)) t s proof (prove)
using this:
(epptr, TCBBlockedSend) \<in> state_refs_of s t

goal (1 subgoal):
 1. \<exists>pl. st_tcb_at ((=) (BlockedOnSend epptr pl)) t s proof (state)
this:
\<exists>pl. st_tcb_at ((=) (BlockedOnSend epptr pl)) t s

goal:
No subgoals!
theory Ipc_AC

lemma receive_ipc_valid_ep_helper:
  "\<lbrakk> invs s; ko_at (Endpoint (SendEP list)) epptr s \<rbrakk>
     \<Longrightarrow> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # t \<Rightarrow> SendEP (tl list)) s" apply (drule_tac invs_valid_objs) apply (drule ko_atD) apply (erule(1) valid_objsE) apply (cases list, solves \<open>simp add: valid_obj_def valid_ep_def\<close>) by (cases "tl list"; clarsimp simp:valid_obj_def valid_ep_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; ko_at (Endpoint (SendEP list)) epptr s\<rbrakk> \<Longrightarrow> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # t \<Rightarrow> SendEP (tl list)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (Endpoint (SendEP list)) epptr s; valid_objs s\<rbrakk> \<Longrightarrow> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # t \<Rightarrow> SendEP (tl list)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; kheap s epptr = Some (Endpoint (SendEP list))\<rbrakk> \<Longrightarrow> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # t \<Rightarrow> SendEP (tl list)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s epptr = Some (Endpoint (SendEP list)); valid_obj epptr (Endpoint (SendEP list)) s\<rbrakk> \<Longrightarrow> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # t \<Rightarrow> SendEP (tl list)) s proof (prove)
goal (1 subgoal):
 1. \<And>a lista. \<lbrakk>kheap s epptr = Some (Endpoint (SendEP list)); valid_obj epptr (Endpoint (SendEP list)) s; list = a # lista\<rbrakk> \<Longrightarrow> valid_ep (case tl list of [] \<Rightarrow> IdleEP | a # t \<Rightarrow> SendEP (tl list)) s
theory Ipc_AC

lemma receive_ipc_sender_helper:
  "\<lbrakk> pas_refined aag s; kheap s thread = Some (TCB tcb); tcb_state tcb = BlockedOnSend ep pl \<rbrakk>
     \<Longrightarrow> abs_has_auth_to aag SyncSend thread ep" apply (erule pas_refined_mem[rotated]) apply (rule sta_ts) apply (simp add: thread_st_auth_def tcb_states_of_state_def get_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; kheap s thread = Some (TCB tcb); tcb_state tcb = BlockedOnSend ep pl\<rbrakk> \<Longrightarrow> (pasObjectAbs aag thread, SyncSend, pasObjectAbs aag ep) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s thread = Some (TCB tcb); tcb_state tcb = BlockedOnSend ep pl\<rbrakk> \<Longrightarrow> (thread, SyncSend, ep) \<in> state_objs_to_policy s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s thread = Some (TCB tcb); tcb_state tcb = BlockedOnSend ep pl\<rbrakk> \<Longrightarrow> (ep, SyncSend) \<in> thread_st_auth s thread proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma receive_ipc_sender_can_grant_helper:
  "\<lbrakk> invs s; pas_refined aag s; kheap s thread = Some (TCB tcb);
     tcb_state tcb = BlockedOnSend ep pl; sender_can_grant pl; aag_has_auth_to aag Receive ep \<rbrakk>
     \<Longrightarrow> is_subject aag thread" apply (frule pas_refined_mem[rotated,where x = "thread" and auth=Grant]) apply (rule sta_ts) apply (simp add:thread_st_auth_def tcb_states_of_state_def get_tcb_def) apply (frule(2) aag_wellformed_grant_Control_to_send[OF _ _ pas_refined_wellformed]) apply (simp add:aag_has_Control_iff_owns) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; pas_refined aag s; kheap s thread = Some (TCB tcb); tcb_state tcb = BlockedOnSend ep pl; sender_can_grant pl; (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag thread proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; pas_refined aag s; kheap s thread = Some (TCB tcb); tcb_state tcb = BlockedOnSend ep pl; sender_can_grant pl; (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (thread, Grant, ?y) \<in> state_objs_to_policy s
 2. \<lbrakk>invs s; pas_refined aag s; kheap s thread = Some (TCB tcb); tcb_state tcb = BlockedOnSend ep pl; sender_can_grant pl; (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; (pasObjectAbs aag thread, Grant, pasObjectAbs aag ?y) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag thread proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; pas_refined aag s; kheap s thread = Some (TCB tcb); tcb_state tcb = BlockedOnSend ep pl; sender_can_grant pl; (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (?y, Grant) \<in> thread_st_auth s thread
 2. \<lbrakk>invs s; pas_refined aag s; kheap s thread = Some (TCB tcb); tcb_state tcb = BlockedOnSend ep pl; sender_can_grant pl; (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; (pasObjectAbs aag thread, Grant, pasObjectAbs aag ?y) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag thread proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; pas_refined aag s; kheap s thread = Some (TCB tcb); tcb_state tcb = BlockedOnSend ep pl; sender_can_grant pl; (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; (pasObjectAbs aag thread, Grant, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag thread proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; pas_refined aag s; kheap s thread = Some (TCB tcb); tcb_state tcb = BlockedOnSend ep pl; sender_can_grant pl; (pasSubject aag, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag; (pasObjectAbs aag thread, Grant, pasObjectAbs aag ep) \<in> pasPolicy aag; (pasSubject aag, Control, pasObjectAbs aag thread) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag thread proof (prove)
goal:
No subgoals!