kings-crown/FVELER_Isabelle huggingface dataset:
theory Access_AC

lemma is_subject_into_is_subject_asid:
  "\<lbrakk> cap_links_asid_slot aag (pasObjectAbs aag p) cap;
     is_subject aag p; pas_refined aag s; asid \<in> cap_asid' cap \<rbrakk>
     \<Longrightarrow> is_subject_asid aag asid" apply (clarsimp simp add: cap_links_asid_slot_def label_owns_asid_slot_def) apply (drule (1) bspec) apply (drule (1) pas_refined_Control) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_links_asid_slot aag (pasObjectAbs aag p) cap; is_subject aag p; pas_refined aag s; asid \<in> cap_asid' cap\<rbrakk> \<Longrightarrow> is_subject_asid aag asid proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>asid\<in>cap_asid' cap. (pasSubject aag, Control, pasASIDAbs aag asid) \<in> pasPolicy aag; is_subject aag p; pas_refined aag s; asid \<in> cap_asid' cap\<rbrakk> \<Longrightarrow> is_subject_asid aag asid proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag p; pas_refined aag s; asid \<in> cap_asid' cap; (pasSubject aag, Control, pasASIDAbs aag asid) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject_asid aag asid proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag p; pas_refined aag s; asid \<in> cap_asid' cap; pasSubject aag = pasASIDAbs aag asid\<rbrakk> \<Longrightarrow> is_subject_asid aag asid proof (prove)
goal:
No subgoals!
theory Access_AC

lemma clas_no_asid:
  "cap_asid' cap = {} \<Longrightarrow> cap_links_asid_slot aag l cap" unfolding cap_links_asid_slot_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_asid' cap = {} \<Longrightarrow> cap_links_asid_slot aag l cap proof (prove)
goal (1 subgoal):
 1. cap_asid' cap = {} \<Longrightarrow> \<forall>asid\<in>cap_asid' cap. label_owns_asid_slot aag l asid
theory Access_AC

lemma cli_no_irqs:
  "cap_irqs_controlled cap = {} \<Longrightarrow> cap_links_irq aag l cap" unfolding cap_links_irq_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_irqs_controlled cap = {} \<Longrightarrow> cap_links_irq aag l cap proof (prove)
goal (1 subgoal):
 1. cap_irqs_controlled cap = {} \<Longrightarrow> \<forall>irq\<in>cap_irqs_controlled cap. (l, Control, pasIRQAbs aag irq) \<in> pasPolicy aag
theory Access_AC

lemma as_user_tcb_states[wp]:
  "as_user t f \<lbrace>\<lambda>s. P (tcb_states_of_state s)\<rbrace>" apply (simp add: as_user_def) apply (wpsimp wp: set_object_wp) apply (clarsimp simp: thread_st_auth_def get_tcb_def tcb_states_of_state_def
                 elim!: rsubst[where P=P, OF _ ext] split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (tcb_states_of_state s)\<rbrace> as_user t f \<lbrace>\<lambda>_ s. P (tcb_states_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (tcb_states_of_state s)\<rbrace> do tcb <- gets_the (get_tcb t);
(a, uc') <- select_f (f (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object t (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>));
return a
od \<lbrace>\<lambda>_ s. P (tcb_states_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y x xa. \<lbrakk>P (tcb_states_of_state s); (x, xa) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); get_tcb t s = Some y\<rbrakk> \<Longrightarrow> P (tcb_states_of_state (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch y)\<rparr>))\<rparr>)) proof (prove)
goal:
No subgoals!
theory Access_AC

lemma as_user_thread_state[wp]:
  "as_user t f \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace>" apply (simp add: thread_st_auth_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace> as_user t f \<lbrace>\<lambda>_ s. P (thread_st_auth s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (case_option {} tcb_st_to_auth \<circ> tcb_states_of_state s)\<rbrace> as_user t f \<lbrace>\<lambda>_ s. P (case_option {} tcb_st_to_auth \<circ> tcb_states_of_state s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Access_AC

lemma as_user_thread_bound_ntfn[wp]:
  "as_user t f \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace>" apply (simp add: as_user_def set_object_def split_def thread_bound_ntfns_def) apply (wp get_object_wp) apply (clarsimp simp: thread_st_auth_def get_tcb_def
                 elim!: rsubst[where P=P, OF _ ext] split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> as_user t f \<lbrace>\<lambda>_ s. P (thread_bound_ntfns s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (\<lambda>p. case get_tcb p s of None \<Rightarrow> None | Some x2 \<Rightarrow> tcb_bound_notification x2)\<rbrace> do tcb <- gets_the (get_tcb t);
p <- select_f (f (arch_tcb_context_get (tcb_arch tcb)));
y <- do kobj <- get_object t;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>))\<rparr>)
od;
return (fst p)
od \<lbrace>\<lambda>_ s. P (\<lambda>p. case get_tcb p s of None \<Rightarrow> None | Some x2 \<Rightarrow> tcb_bound_notification x2)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (\<lambda>p. case get_tcb p s of None \<Rightarrow> None | Some x2 \<Rightarrow> tcb_bound_notification x2) \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). \<forall>ko. ko_at ko t s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (\<lambda>p. case get_tcb p (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb t s)))\<rparr>))\<rparr>) of None \<Rightarrow> None | Some x2 \<Rightarrow> tcb_bound_notification x2)) proof (prove)
goal:
No subgoals!
theory Access_AC

lemma tcb_domain_map_wellformed_lift:
  assumes 1: "\<And>P. f \<lbrace>\<lambda>s. P (ekheap s)\<rbrace>"
  shows "f \<lbrace>tcb_domain_map_wellformed aag\<rbrace>" by (rule 1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_domain_map_wellformed aag\<rbrace> f \<lbrace>\<lambda>_. tcb_domain_map_wellformed aag\<rbrace>
theory Access_AC

lemma bang_0_in_set:
  "xs \<noteq> [] \<Longrightarrow> xs ! 0 \<in> set xs" by (fastforce simp: in_set_conv_nth)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> xs ! 0 \<in> set xs
theory Access_AC

lemma update_one_strg:
  "(b \<longrightarrow> P c v) \<and> (\<not> b \<longrightarrow> (\<forall>v'. f c' = Some v' \<longrightarrow> P c v'))
   \<longrightarrow> ((f(c := if b then Some v else f c')) x = Some y \<and> f x \<noteq> Some y \<longrightarrow> P x y)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (b \<longrightarrow> P c v) \<and> (\<not> b \<longrightarrow> (\<forall>v'. f c' = Some v' \<longrightarrow> P c v')) \<longrightarrow> (f(c := if b then Some v else f c')) x = Some y \<and> f x \<noteq> Some y \<longrightarrow> P x y
theory Access_AC

lemma hoare_gen_asm2:
  assumes a: "P \<Longrightarrow> \<lbrace>\<top>\<rbrace> f \<lbrace>Q\<rbrace>"
  shows "\<lbrace>K P\<rbrace> f \<lbrace>Q\<rbrace>" using a by (fastforce simp: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K P\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
using this:
P \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> f \<lbrace>Q\<rbrace>

goal (1 subgoal):
 1. \<lbrace>K P\<rbrace> f \<lbrace>Q\<rbrace>
theory Access_AC

lemma hoare_vcg_all_liftE:
  "(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>, \<lbrace>Q' x\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>, \<lbrace>\<lambda>rv s. \<forall>x. Q' x rv s\<rbrace>" unfolding validE_def apply (rule hoare_post_imp [where Q = "\<lambda>v s. \<forall>x. case v of Inl e \<Rightarrow> Q' x e s | Inr r \<Rightarrow> Q x r s"]) apply (clarsimp split: sum.splits) apply (erule hoare_vcg_all_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>, \<lbrace>Q' x\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>, \<lbrace>\<lambda>rv s. \<forall>x. Q' x rv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' x e s | Inr r \<Rightarrow> Q x r s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> \<forall>x. Q' x e s | Inr r \<Rightarrow> \<forall>x. Q x r s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' x e s | Inr r \<Rightarrow> Q x r s\<rbrace>; \<forall>x. case rv of Inl e \<Rightarrow> Q' x e s | Inr r \<Rightarrow> Q x r s\<rbrakk> \<Longrightarrow> case rv of Inl e \<Rightarrow> \<forall>x. Q' x e s | Inr r \<Rightarrow> \<forall>x. Q x r s
 2. (\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' x e s | Inr r \<Rightarrow> Q x r s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>v s. \<forall>x. case v of Inl e \<Rightarrow> Q' x e s | Inr r \<Rightarrow> Q x r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' x e s | Inr r \<Rightarrow> Q x r s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>v s. \<forall>x. case v of Inl e \<Rightarrow> Q' x e s | Inr r \<Rightarrow> Q x r s\<rbrace> proof (prove)
goal:
No subgoals!
theory Access_AC

lemma mapM_x_and_const_wp:
  assumes f: "\<And>v. \<lbrace>P and K (Q v)\<rbrace> f v \<lbrace>\<lambda>rv. P\<rbrace>"
  shows "\<lbrace>P and K (\<forall>v \<in> set vs. Q v)\<rbrace> mapM_x f vs \<lbrace>\<lambda>rv. P\<rbrace>" apply (induct vs) apply (simp add: mapM_x_Nil) apply (simp add: mapM_x_Cons) apply (wp f | assumption | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and K (\<forall>v\<in>set vs. Q v)\<rbrace> mapM_x f vs \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>P and K (\<forall>v\<in>set []. Q v)\<rbrace> mapM_x f [] \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>a vs. \<lbrace>P and K (\<forall>v\<in>set vs. Q v)\<rbrace> mapM_x f vs \<lbrace>\<lambda>rv. P\<rbrace> \<Longrightarrow> \<lbrace>P and K (\<forall>v\<in>set (a # vs). Q v)\<rbrace> mapM_x f (a # vs) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a vs. \<lbrace>P and K (\<forall>v\<in>set vs. Q v)\<rbrace> mapM_x f vs \<lbrace>\<lambda>rv. P\<rbrace> \<Longrightarrow> \<lbrace>P and K (\<forall>v\<in>set (a # vs). Q v)\<rbrace> mapM_x f (a # vs) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a vs. \<lbrace>\<lambda>a. P a \<and> Ball (set vs) Q\<rbrace> mapM_x f vs \<lbrace>\<lambda>rv. P\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>b. P b \<and> Q a \<and> Ball (set vs) Q\<rbrace> do y <- f a;
mapM_x f vs
od \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Access_AC

lemma ep_queued_st_tcb_at':
  "\<And>P. \<lbrakk> ko_at (Endpoint ep) ptr s; (t, rt) \<in> ep_q_refs_of ep;
         valid_objs s; sym_refs (state_refs_of s);
         \<And>pl pl'. P (BlockedOnSend ptr pl) \<and> P (BlockedOnReceive ptr pl') \<rbrakk>
         \<Longrightarrow> st_tcb_at P t s" apply (case_tac ep, simp_all) apply (frule(1) sym_refs_ko_atD, clarsimp, erule (1) my_BallE,
         clarsimp simp: st_tcb_at_def refs_of_rev elim!: obj_at_weakenE)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>ko_at (Endpoint ep) ptr s; (t, rt) \<in> ep_q_refs_of ep; valid_objs s; sym_refs (state_refs_of s); \<And>pl pl'. P (BlockedOnSend ptr pl) \<and> P (BlockedOnReceive ptr pl')\<rbrakk> \<Longrightarrow> st_tcb_at P t s proof (prove)
goal (2 subgoals):
 1. \<And>P x2. \<lbrakk>ko_at (Endpoint (SendEP x2)) ptr s; t \<in> set x2 \<and> rt = EPSend; valid_objs s; sym_refs (state_refs_of s); \<And>pl pl'. P (BlockedOnSend ptr pl) \<and> P (BlockedOnReceive ptr pl'); ep = SendEP x2\<rbrakk> \<Longrightarrow> st_tcb_at P t s
 2. \<And>P x3. \<lbrakk>ko_at (Endpoint (RecvEP x3)) ptr s; t \<in> set x3 \<and> rt = EPRecv; valid_objs s; sym_refs (state_refs_of s); \<And>pl pl'. P (BlockedOnSend ptr pl) \<and> P (BlockedOnReceive ptr pl'); ep = RecvEP x3\<rbrakk> \<Longrightarrow> st_tcb_at P t s proof (prove)
goal:
No subgoals!
theory Access_AC

lemma ep_rcv_queued_st_tcb_at:
  "\<And>P. \<lbrakk> ko_at (Endpoint ep) epptr s; (t, EPRecv) \<in> ep_q_refs_of ep;
         valid_objs s; sym_refs (state_refs_of s);
         \<And>pl. P (BlockedOnReceive epptr pl); kheap s' t = kheap s t\<rbrakk>
         \<Longrightarrow> st_tcb_at P t s'" apply (case_tac ep, simp_all) apply (subgoal_tac "st_tcb_at P t s") apply (simp add: st_tcb_at_def obj_at_def) apply (frule(1) sym_refs_ko_atD, clarsimp, erule (1) my_BallE,
         clarsimp simp: st_tcb_at_def refs_of_rev elim!: obj_at_weakenE)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>ko_at (Endpoint ep) epptr s; (t, EPRecv) \<in> ep_q_refs_of ep; valid_objs s; sym_refs (state_refs_of s); \<And>pl. P (BlockedOnReceive epptr pl); kheap s' t = kheap s t\<rbrakk> \<Longrightarrow> st_tcb_at P t s' proof (prove)
goal (1 subgoal):
 1. \<And>P x3. \<lbrakk>ko_at (Endpoint (RecvEP x3)) epptr s; t \<in> set x3; valid_objs s; sym_refs (state_refs_of s); \<And>pl. P (BlockedOnReceive epptr pl); kheap s' t = kheap s t; ep = RecvEP x3\<rbrakk> \<Longrightarrow> st_tcb_at P t s' proof (prove)
goal (2 subgoals):
 1. \<And>P x3. \<lbrakk>ko_at (Endpoint (RecvEP x3)) epptr s; t \<in> set x3; valid_objs s; sym_refs (state_refs_of s); \<And>pl. P (BlockedOnReceive epptr pl); kheap s' t = kheap s t; ep = RecvEP x3; st_tcb_at P t s\<rbrakk> \<Longrightarrow> st_tcb_at P t s'
 2. \<And>P x3. \<lbrakk>ko_at (Endpoint (RecvEP x3)) epptr s; t \<in> set x3; valid_objs s; sym_refs (state_refs_of s); \<And>pl. P (BlockedOnReceive epptr pl); kheap s' t = kheap s t; ep = RecvEP x3\<rbrakk> \<Longrightarrow> st_tcb_at P t s proof (prove)
goal (1 subgoal):
 1. \<And>P x3. \<lbrakk>ko_at (Endpoint (RecvEP x3)) epptr s; t \<in> set x3; valid_objs s; sym_refs (state_refs_of s); \<And>pl. P (BlockedOnReceive epptr pl); kheap s' t = kheap s t; ep = RecvEP x3\<rbrakk> \<Longrightarrow> st_tcb_at P t s proof (prove)
goal:
No subgoals!
theory Access_AC

lemma ntfn_queued_st_tcb_at':
  "\<And>P. \<lbrakk> ko_at (Notification ntfn) ntfnptr s; (t, rt) \<in> ntfn_q_refs_of (ntfn_obj ntfn);
         valid_objs s; sym_refs (state_refs_of s); P (BlockedOnNotification ntfnptr) \<rbrakk>
         \<Longrightarrow> st_tcb_at P t s" apply (case_tac "ntfn_obj ntfn", simp_all) apply (frule(1) sym_refs_ko_atD) apply (clarsimp) apply (erule_tac y="(t, NTFNSignal)" in my_BallE, clarsimp) apply (clarsimp simp: pred_tcb_at_def refs_of_rev elim!: obj_at_weakenE)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; (t, rt) \<in> ntfn_q_refs_of (ntfn_obj ntfn); valid_objs s; sym_refs (state_refs_of s); P (BlockedOnNotification ntfnptr)\<rbrakk> \<Longrightarrow> st_tcb_at P t s proof (prove)
goal (1 subgoal):
 1. \<And>P x2. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set x2 \<and> rt = NTFNSignal; valid_objs s; sym_refs (state_refs_of s); P (BlockedOnNotification ntfnptr); ntfn_obj ntfn = WaitingNtfn x2\<rbrakk> \<Longrightarrow> st_tcb_at P t s proof (prove)
goal (1 subgoal):
 1. \<And>P x2. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; t \<in> set x2 \<and> rt = NTFNSignal; valid_objs s; sym_refs (state_refs_of s); P (BlockedOnNotification ntfnptr); ntfn_obj ntfn = WaitingNtfn x2; state_refs_of s ntfnptr = refs_of (Notification ntfn) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ntfn). obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x s)\<rbrakk> \<Longrightarrow> st_tcb_at P t s proof (prove)
goal (1 subgoal):
 1. \<And>P x2. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; sym_refs (state_refs_of s); P (BlockedOnNotification ntfnptr); ntfn_obj ntfn = WaitingNtfn x2; t \<in> set x2; rt = NTFNSignal; state_refs_of s ntfnptr = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn); \<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x s\<rbrakk> \<Longrightarrow> st_tcb_at P t s proof (prove)
goal (1 subgoal):
 1. \<And>P x2. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; sym_refs (state_refs_of s); P (BlockedOnNotification ntfnptr); ntfn_obj ntfn = WaitingNtfn x2; t \<in> set x2; rt = NTFNSignal; state_refs_of s ntfnptr = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn); case (t, NTFNSignal) of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x s\<rbrakk> \<Longrightarrow> st_tcb_at P t s proof (prove)
goal:
No subgoals!
theory Access_AC

lemma case_prod_wp:
  "(\<And>a b. x = (a, b) \<Longrightarrow> \<lbrace>P a b\<rbrace> f a b \<lbrace>Q\<rbrace>)
   \<Longrightarrow> \<lbrace>P (fst x) (snd x)\<rbrace> case_prod f x \<lbrace>Q\<rbrace>" by (cases x, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. x = (a, b) \<Longrightarrow> \<lbrace>P a b\<rbrace> f a b \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P (fst x) (snd x)\<rbrace> case x of (x, xa) \<Rightarrow> f x xa \<lbrace>Q\<rbrace>
theory Access_AC

lemma case_sum_wp:
  "\<lbrakk> (\<And>a. x = Inl a \<Longrightarrow> \<lbrace>P a\<rbrace> f a \<lbrace>Q\<rbrace>); (\<And>a. x = Inr a \<Longrightarrow> \<lbrace>P' a\<rbrace> g a \<lbrace>Q\<rbrace>) \<rbrakk>
     \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>a. x = Inl a \<longrightarrow> P a s) \<and> (\<forall>a. x = Inr a \<longrightarrow> P' a s)\<rbrace> case_sum f g x \<lbrace>Q\<rbrace>" by (cases x, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. x = Inl a \<Longrightarrow> \<lbrace>P a\<rbrace> f a \<lbrace>Q\<rbrace>; \<And>a. x = Inr a \<Longrightarrow> \<lbrace>P' a\<rbrace> g a \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>a. x = Inl a \<longrightarrow> P a s) \<and> (\<forall>a. x = Inr a \<longrightarrow> P' a s)\<rbrace> case x of Inl x \<Rightarrow> f x | Inr x \<Rightarrow> g x \<lbrace>Q\<rbrace>
theory Access_AC

lemma st_tcb_at_to_thread_st_auth:
  "st_tcb_at P t s \<Longrightarrow> \<exists>st. P st \<and> thread_st_auth s t = tcb_st_to_auth st" by (fastforce simp: st_tcb_def2 thread_st_auth_def tcb_states_of_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at P t s \<Longrightarrow> \<exists>st. P st \<and> thread_st_auth s t = tcb_st_to_auth st
theory Access_AC

lemma aag_Control_into_owns:
  "\<lbrakk> aag_has_auth_to aag Control p; pas_refined aag s \<rbrakk> \<Longrightarrow> is_subject aag p" apply (drule (1) pas_refined_Control) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, Control, pasObjectAbs aag p) \<in> pasPolicy aag; pas_refined aag s\<rbrakk> \<Longrightarrow> is_subject aag p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; pasSubject aag = pasObjectAbs aag p\<rbrakk> \<Longrightarrow> is_subject aag p proof (prove)
goal:
No subgoals!
theory Access_AC

lemma aag_has_Control_iff_owns:
  "pas_refined aag s \<Longrightarrow> (aag_has_auth_to aag Control x) = (is_subject aag x)" apply (rule iffI) apply (erule (1) aag_Control_into_owns) apply (simp add: pas_refined_refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined aag s \<Longrightarrow> ((pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) = is_subject aag x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag x
 2. \<lbrakk>pas_refined aag s; is_subject aag x\<rbrakk> \<Longrightarrow> (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; is_subject aag x\<rbrakk> \<Longrightarrow> (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!
theory Access_AC

lemma aag_Control_owns_strg:
  "pas_wellformed aag \<and> is_subject aag v \<longrightarrow> aag_has_auth_to aag Control v" by (clarsimp simp: aag_wellformed_refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_wellformed aag \<and> is_subject aag v \<longrightarrow> (pasSubject aag, Control, pasObjectAbs aag v) \<in> pasPolicy aag
theory Access_AC

lemma cli_caps_of_state:
  "\<lbrakk> caps_of_state s slot = Some cap; pas_refined aag s \<rbrakk>
     \<Longrightarrow> cap_links_irq aag (pasObjectAbs aag (fst slot)) cap" apply (clarsimp simp add: cap_links_irq_def pas_refined_def) apply (blast dest: state_irqs_to_policy_aux.intros) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s slot = Some cap; pas_refined aag s\<rbrakk> \<Longrightarrow> cap_links_irq aag (pasObjectAbs aag (fst slot)) cap proof (prove)
goal (1 subgoal):
 1. \<And>irq. \<lbrakk>caps_of_state s slot = Some cap; irq \<in> cap_irqs_controlled cap; pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst slot), Control, pasIRQAbs aag irq) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!
theory Access_AC

lemma cap_cur_auth_caps_of_state:
  "\<lbrakk> caps_of_state s p = Some cap; pas_refined aag s; is_subject aag (fst p) \<rbrakk>
     \<Longrightarrow> pas_cap_cur_auth aag cap" by (metis cap_auth_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; pas_refined aag s; is_subject aag (fst p)\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag cap
theory Access_AC

lemma tcb_bound_notification_reset_integrity_mono:
  "\<lbrakk> tcb_bound_notification_reset_integrity ntfn ntfn' S aag; S \<subseteq> T\<rbrakk>
     \<Longrightarrow> tcb_bound_notification_reset_integrity ntfn ntfn' T aag" unfolding tcb_bound_notification_reset_integrity_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_bound_notification_reset_integrity ntfn ntfn' S aag; S \<subseteq> T\<rbrakk> \<Longrightarrow> tcb_bound_notification_reset_integrity ntfn ntfn' T aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ntfn = ntfn' \<or> ntfn' = None \<and> aag_subjects_have_auth_to S aag Reset (the ntfn); S \<subseteq> T\<rbrakk> \<Longrightarrow> ntfn = ntfn' \<or> ntfn' = None \<and> aag_subjects_have_auth_to T aag Reset (the ntfn)
theory Access_AC

lemma reply_cap_deletion_integrity_mono:
  "\<lbrakk> reply_cap_deletion_integrity S aag cap cap'; S \<subseteq> T \<rbrakk>
     \<Longrightarrow> reply_cap_deletion_integrity T aag cap cap'" by (blast intro: reply_cap_deletion_integrity_intros elim: reply_cap_deletion_integrityE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reply_cap_deletion_integrity S aag cap cap'; S \<subseteq> T\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity T aag cap cap'
theory Access_AC

lemma cnode_integrity_mono:
  "\<lbrakk> cnode_integrity S aag cont cont'; S \<subseteq> T\<rbrakk> \<Longrightarrow> cnode_integrity T aag cont cont'" by (blast intro!: cnode_integrityI elim: cnode_integrityE dest: reply_cap_deletion_integrity_mono)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cnode_integrity S aag cont cont'; S \<subseteq> T\<rbrakk> \<Longrightarrow> cnode_integrity T aag cont cont'