kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_AC

lemma set_notification_respects:
  "\<lbrace>integrity aag X st and K (aag_has_auth_to aag auth epptr \<and> auth \<in> {Receive, Notify, Reset})\<rbrace>
   set_notification epptr ntfn'
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: set_simple_ko_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: obj_at_def partial_inv_def a_type_def) apply (erule integrity_trans) apply (clarsimp simp: integrity_def tro_ntfn integrity_asids_kh_upds) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K ((pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> auth \<in> {Receive, Notify, Reset})\<rbrace> set_notification epptr ntfn' \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>y. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify \<or> auth = Reset))\<rbrace> do obj <- get_object epptr;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. Notification y = obj);
kobj <- get_object epptr;
y <- assert (a_type kobj = ANTFN);
s <- get;
put (s\<lparr>kheap := (kheap s)(epptr \<mapsto> Notification ntfn')\<rparr>)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity aag X st and (\<lambda>y. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify \<or> auth = Reset))) s \<Longrightarrow> \<forall>ko. ko_at ko epptr s \<longrightarrow> a_type ko = AEndpoint \<or> a_type ko = ANTFN \<longrightarrow> (\<exists>y. Notification y = ko) \<longrightarrow> (\<forall>ko. ko_at ko epptr s \<longrightarrow> a_type ko = ANTFN \<longrightarrow> integrity aag X st (s\<lparr>kheap := (kheap s)(epptr \<mapsto> Notification ntfn')\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>integrity aag X st s; (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; auth = Receive \<or> auth = Notify \<or> auth = Reset; kheap s epptr = Some (Notification y)\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := \<lambda>a. if a = epptr then Some (Notification ntfn') else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>(pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag; auth = Receive \<or> auth = Notify \<or> auth = Reset; kheap s epptr = Some (Notification y)\<rbrakk> \<Longrightarrow> integrity aag X s (s\<lparr>kheap := \<lambda>a. if a = epptr then Some (Notification ntfn') else kheap s a\<rparr>) proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma set_notification_obj_at:
  "\<lbrace>obj_at P ptr and K (ptr \<noteq> ntfnptr)\<rbrace>
   set_notification ntfnptr queue
   \<lbrace>\<lambda>_. obj_at P ptr\<rbrace>" apply (simp add: set_simple_ko_def set_object_def) apply (wp get_object_wp) apply (auto simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at P ptr and K (ptr \<noteq> ntfnptr)\<rbrace> set_notification ntfnptr queue \<lbrace>\<lambda>_. obj_at P ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at P ptr and (\<lambda>y. ptr \<noteq> ntfnptr)\<rbrace> do obj <- get_object ntfnptr;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. Notification y = obj);
kobj <- get_object ntfnptr;
y <- assert (a_type kobj = ANTFN);
s <- get;
put (s\<lparr>kheap := (kheap s)(ntfnptr \<mapsto> Notification queue)\<rparr>)
od \<lbrace>\<lambda>_. obj_at P ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (obj_at P ptr and (\<lambda>y. ptr \<noteq> ntfnptr)) s \<Longrightarrow> \<forall>ko. ko_at ko ntfnptr s \<longrightarrow> a_type ko = AEndpoint \<or> a_type ko = ANTFN \<longrightarrow> (\<exists>y. Notification y = ko) \<longrightarrow> (\<forall>ko. ko_at ko ntfnptr s \<longrightarrow> a_type ko = ANTFN \<longrightarrow> obj_at P ptr (s\<lparr>kheap := (kheap s)(ntfnptr \<mapsto> Notification queue)\<rparr>)) proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma set_ntfn_valid_objs_at:
  "\<lbrace>valid_objs and (\<lambda>s. ntfn_at p s \<longrightarrow> valid_ntfn ntfn s)\<rbrace>
   set_notification p ntfn
   \<lbrace>\<lambda>rv. valid_objs\<rbrace>" unfolding set_simple_ko_def apply (rule hoare_pre) apply (wp set_object_valid_objs get_object_wp) apply (clarsimp simp: valid_obj_def obj_at_def is_ntfn partial_inv_def
                 split: kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and (\<lambda>s. ntfn_at p s \<longrightarrow> valid_ntfn ntfn s)\<rbrace> set_notification p ntfn \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and (\<lambda>s. ntfn_at p s \<longrightarrow> valid_ntfn ntfn s)\<rbrace> do obj <- get_object p;
assert (is_simple_type obj);
assert (partial_inv Notification obj \<noteq> None);
set_object p (Notification ntfn)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do obj <- get_object p;
assert (is_simple_type obj);
assert (partial_inv Notification obj \<noteq> None);
set_object p (Notification ntfn)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace>
 2. \<And>s. (valid_objs and (\<lambda>s. ntfn_at p s \<longrightarrow> valid_ntfn ntfn s)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs and (\<lambda>s. ntfn_at p s \<longrightarrow> valid_ntfn ntfn s)) s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> is_simple_type ko \<longrightarrow> partial_inv Notification ko \<noteq> None \<longrightarrow> (valid_objs and valid_obj p (Notification ntfn)) s proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma set_thread_state_integrity_once_ts_upd:
  "set_thread_state t ts' \<lbrace>integrity_once_ts_upd t ts aag X st\<rbrace>" apply (simp add: set_thread_state_def) apply (wpsimp wp: set_object_wp set_thread_state_ext_integrity_once_ts_upd) apply (clarsimp simp: fun_upd_def dest!: get_tcb_SomeD) apply (simp add: get_tcb_def cong: if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_once_ts_upd t ts aag X st\<rbrace> set_thread_state t ts' \<lbrace>\<lambda>_. integrity_once_ts_upd t ts aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_once_ts_upd t ts aag X st\<rbrace> do tcb <- gets_the (get_tcb t);
y <- set_object t (TCB (tcb\<lparr>tcb_state := ts'\<rparr>));
set_thread_state_ext t
od \<lbrace>\<lambda>_. integrity_once_ts_upd t ts aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>integrity aag X st (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_state := ts\<rparr>))\<rparr>); get_tcb t s = Some y\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_state := ts'\<rparr>))\<rparr>))\<lparr>tcb_state := ts\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>integrity aag X st (s\<lparr>kheap := \<lambda>x. if x = t then Some (TCB (y\<lparr>tcb_state := ts\<rparr>)) else kheap s x\<rparr>); kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t (s\<lparr>kheap := \<lambda>x. if x = t then Some (TCB (y\<lparr>tcb_state := ts'\<rparr>)) else kheap s x\<rparr>))\<lparr>tcb_state := ts\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma get_tcb_recv_blocked_implies_receive:
  "\<lbrakk> pas_refined aag s; get_tcb t s = Some tcb; ep_recv_blocked ep (tcb_state tcb) \<rbrakk>
     \<Longrightarrow> abs_has_auth_to aag Receive t ep" apply (erule pas_refined_mem[rotated]) apply (rule sta_ts) apply (simp add: thread_st_auth_def tcb_states_of_state_def) apply (case_tac "tcb_state tcb", simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; get_tcb t s = Some tcb; ep_recv_blocked ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag t, Receive, pasObjectAbs aag ep) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_tcb t s = Some tcb; ep_recv_blocked ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> (t, Receive, ep) \<in> state_objs_to_policy s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_tcb t s = Some tcb; ep_recv_blocked ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> (ep, Receive) \<in> thread_st_auth s t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_tcb t s = Some tcb; ep_recv_blocked ep (tcb_state tcb)\<rbrakk> \<Longrightarrow> (ep, Receive) \<in> tcb_st_to_auth (tcb_state tcb) proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma set_thread_state_integrity':
  "\<lbrace>integrity_once_ts_upd t ts aag X st\<rbrace> set_thread_state t ts \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: set_thread_state_def) by (wpsimp wp: set_object_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_once_ts_upd t ts aag X st\<rbrace> set_thread_state t ts \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_once_ts_upd t ts aag X st\<rbrace> do tcb <- gets_the (get_tcb t);
y <- set_object t (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext t
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory Ipc_AC

lemma tba_Some:
  "thread_bound_ntfns s t = Some a \<Longrightarrow> bound_tcb_at ((=) (Some a)) t s" by (clarsimp simp: thread_bound_ntfns_def pred_tcb_at_def obj_at_def get_tcb_def
              split: option.splits kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_bound_ntfns s t = Some a \<Longrightarrow> bound_tcb_at ((=) (Some a)) t s
theory Ipc_AC

lemma cap_badge_masked_as_full:
  "(cap_badge (masked_as_full a a), cap_badge a) \<in> capBadge_ordering False" by (cases a, simp_all add: masked_as_full_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cap_badge (masked_as_full a a), cap_badge a) \<in> capBadge_ordering False
theory Ipc_AC

lemma masked_as_full_double:
  "masked_as_full (masked_as_full ab ab) cap' = masked_as_full ab ab" by (cases ab, simp_all add: masked_as_full_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. masked_as_full (masked_as_full ab ab) cap' = masked_as_full ab ab
theory Ipc_AC

lemma lookup_slot_for_thread_authorised:
  "\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace>
   lookup_slot_for_thread thread cref
   \<lbrace>\<lambda>rv _. is_subject aag (fst (fst rv))\<rbrace>,-" unfolding lookup_slot_for_thread_def apply wp apply (clarsimp simp: owns_thread_owns_cspace) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace> lookup_slot_for_thread thread cref \<lbrace>\<lambda>rv _. is_subject aag (fst (fst rv))\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace> doE tcb <- liftE $ gets_the $ get_tcb thread;
resolve_address_bits (tcb_ctable tcb, cref)
odE \<lbrace>\<lambda>rv _. is_subject aag (fst (fst rv))\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and K (is_subject aag thread)) s \<Longrightarrow> get_tcb thread s \<noteq> None \<longrightarrow> (pas_refined aag and K (is_cnode_cap (tcb_ctable (the (get_tcb thread s))) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (tcb_ctable (the (get_tcb thread s))). is_subject aag x))) s proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma cnode_cap_all_auth_owns:
  "(\<exists>s. is_cnode_cap cap \<and> pas_refined aag s \<and>
        (\<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. aag_has_auth_to aag auth x))
   \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x)" apply (clarsimp simp: is_cap_simps) apply (clarsimp simp: cap_auth_conferred_def pas_refined_all_auth_is_owns) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>s. is_cnode_cap cap \<and> pas_refined aag s \<and> (\<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag)) \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x) proof (prove)
goal (1 subgoal):
 1. \<And>r bits g s. \<lbrakk>cap = CNodeCap r bits g; \<forall>auth\<in>cap_auth_conferred (CNodeCap r bits g). (pasSubject aag, auth, pasObjectAbs aag r) \<in> pasPolicy aag; pas_refined aag s\<rbrakk> \<Longrightarrow> is_subject aag r proof (prove)
goal:
No subgoals!
theory Ipc_AC

lemma remove_rights_clas[simp]:
  "cap_links_asid_slot aag p (remove_rights R cap) = cap_links_asid_slot aag p cap" unfolding cap_links_asid_slot_def remove_rights_def cap_rights_update_def by (clarsimp split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_links_asid_slot aag p (remove_rights R cap) = cap_links_asid_slot aag p cap proof (prove)
goal (1 subgoal):
 1. (\<forall>asid\<in>cap_asid' (case cap of EndpointCap oref badge cr \<Rightarrow> EndpointCap oref badge (cap_rights cap - R) | NotificationCap oref badge cr \<Rightarrow> NotificationCap oref badge (cap_rights cap - R - {AllowGrant, AllowGrantReply}) | ReplyCap t m cr \<Rightarrow> ReplyCap t m (cap_rights cap - R - {AllowRead, AllowGrantReply} \<union> {AllowWrite}) | ArchObjectCap acap \<Rightarrow> ArchObjectCap (acap_rights_update (cap_rights cap - R) acap) | _ \<Rightarrow> cap). label_owns_asid_slot aag p asid) = (\<forall>asid\<in>cap_asid' cap. label_owns_asid_slot aag p asid)
theory Ipc_AC

lemma remove_rights_cli[simp]:
  "cap_links_irq aag l (remove_rights R cap) = cap_links_irq aag l cap" unfolding remove_rights_def cap_rights_update_def by (clarsimp split: cap.splits simp: cap_links_irq_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_links_irq aag l (remove_rights R cap) = cap_links_irq aag l cap proof (prove)
goal (1 subgoal):
 1. cap_links_irq aag l (case cap of EndpointCap oref badge cr \<Rightarrow> EndpointCap oref badge (cap_rights cap - R) | NotificationCap oref badge cr \<Rightarrow> NotificationCap oref badge (cap_rights cap - R - {AllowGrant, AllowGrantReply}) | ReplyCap t m cr \<Rightarrow> ReplyCap t m (cap_rights cap - R - {AllowRead, AllowGrantReply} \<union> {AllowWrite}) | ArchObjectCap acap \<Rightarrow> ArchObjectCap (acap_rights_update (cap_rights cap - R) acap) | _ \<Rightarrow> cap) = cap_links_irq aag l cap
theory Ipc_AC

lemma remove_rights_untyped_range[simp]:
  "untyped_range (remove_rights R c) = untyped_range c" unfolding remove_rights_def cap_rights_update_def by (clarsimp split: cap.splits simp: cap_links_irq_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_range (remove_rights R c) = untyped_range c proof (prove)
goal (1 subgoal):
 1. untyped_range (case c of EndpointCap oref badge cr \<Rightarrow> EndpointCap oref badge (cap_rights c - R) | NotificationCap oref badge cr \<Rightarrow> NotificationCap oref badge (cap_rights c - R - {AllowGrant, AllowGrantReply}) | ReplyCap t m cr \<Rightarrow> ReplyCap t m (cap_rights c - R - {AllowRead, AllowGrantReply} \<union> {AllowWrite}) | ArchObjectCap acap \<Rightarrow> ArchObjectCap (acap_rights_update (cap_rights c - R) acap) | _ \<Rightarrow> c) = untyped_range c
theory Ipc_AC

lemma obj_refs_remove_rights[simp]:
  "obj_refs_ac (remove_rights rs cap) = obj_refs_ac cap" unfolding remove_rights_def by (cases cap, simp_all add: cap_rights_update_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_refs_ac (remove_rights rs cap) = obj_refs_ac cap proof (prove)
goal (1 subgoal):
 1. obj_refs_ac (cap_rights_update (cap_rights cap - rs) cap) = obj_refs_ac cap
theory Ipc_AC

lemma remove_rights_cur_auth:
  "pas_cap_cur_auth aag cap \<Longrightarrow> pas_cap_cur_auth aag (remove_rights R cap)" unfolding aag_cap_auth_def by (clarsimp dest!: remove_rights_cap_auth_conferred_subset)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_cap_cur_auth aag cap \<Longrightarrow> pas_cap_cur_auth aag (remove_rights R cap) proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range cap. (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) cap \<and> cap_links_irq aag (pasSubject aag) cap \<Longrightarrow> (\<forall>x\<in>obj_refs_ac (remove_rights R cap). \<forall>auth\<in>cap_auth_conferred (remove_rights R cap). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (remove_rights R cap). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (remove_rights R cap) \<and> cap_links_irq aag (pasSubject aag) (remove_rights R cap)
theory Ipc_AC

lemma derive_cap_is_transferable:
  "\<lbrace>K (is_transferable_cap cap)\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv _. is_transferable_cap rv\<rbrace>, -" apply (rule hoare_gen_asmE2) by (erule is_transferable_capE; wpsimp simp: derive_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_transferable_cap cap)\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv _. is_transferable_cap rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. is_transferable_cap cap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv _. is_transferable_cap rv\<rbrace>, -
theory Ipc_AC

lemma auth_derived_refl[simp]:
  "auth_derived cap cap" by (simp add: auth_derived_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. auth_derived cap cap
theory Ipc_AC

lemma derive_cap_auth_derived:
  "\<lbrace>\<top>\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s :: det_ext state. rv \<noteq> NullCap \<longrightarrow> auth_derived rv cap\<rbrace>, -" by (cases cap; wpsimp wp: arch_derive_cap_auth_derived simp: derive_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> auth_derived rv cap\<rbrace>, -
theory Ipc_AC

lemma auth_derived_pas_cur_auth:
  "\<lbrakk> auth_derived cap cap'; pas_cap_cur_auth aag cap' \<rbrakk>
     \<Longrightarrow> pas_cap_cur_auth aag cap" by (force simp: aag_cap_auth_def auth_derived_def cap_links_asid_slot_def cap_links_irq_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>auth_derived cap cap'; pas_cap_cur_auth aag cap'\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag cap
theory Ipc_AC

lemma transfer_caps_pas_refined:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs
                    and valid_arch_state and valid_objs and valid_mdb
                    and (\<lambda>s. (\<forall>x \<in> set caps. valid_cap (fst x) s
                                           \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s
                                           \<and> real_cte_at (snd x) s))
                    and K (is_subject aag receiver \<and>
                           (\<forall>x \<in> set caps. is_subject aag (fst (snd x))) \<and>
                           (\<forall>x \<in> set caps. pas_cap_cur_auth aag (fst x)))\<rbrace>
     transfer_caps info caps endpoint receiver recv_buf
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" unfolding transfer_caps_def by (wp transfer_caps_loop_pas_refined get_receive_slots_authorised get_recv_slot_inv
         hoare_vcg_const_imp_lift hoare_vcg_all_lift grs_distinct
      | wpc | simp del: get_receive_slots.simps add: ball_conj_distrib)+

(* 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 (\<lambda>s. \<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) and K (is_subject aag receiver \<and> (\<forall>x\<in>set caps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set caps. pas_cap_cur_auth aag (fst x)))\<rbrace> transfer_caps info caps endpoint receiver recv_buf \<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 (\<lambda>s. \<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) and K (is_subject aag receiver \<and> (\<forall>x\<in>set caps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set caps. pas_cap_cur_auth aag (fst x)))\<rbrace> do dest_slots <- get_receive_slots receiver recv_buf;
mi' <- return $ MI (mi_length info) 0 0 (mi_label info);
case recv_buf of None \<Rightarrow> return mi' | Some receive_buffer \<Rightarrow> transfer_caps_loop endpoint receive_buffer 0 caps dest_slots mi'
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory Ipc_AC

lemma copy_mrs_pas_refined:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace>
   copy_mrs sender sbuf receiver rbuf n
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" unfolding copy_mrs_def apply (rule_tac Q="\<lambda>_. pas_refined aag and pspace_aligned
                                         and valid_vspace_objs
                                         and valid_arch_state"
               in hoare_strengthen_post[rotated], clarsimp) apply (wpsimp wp: mapM_wp_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> copy_mrs sender sbuf receiver rbuf n \<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\<rbrace> do hardware_mrs <- return $ take (unat n) msg_registers;
mapM (\<lambda>r. do v <- as_user sender $ getRegister r;
as_user receiver $ setRegister r v
od) hardware_mrs;
buf_mrs <- case (sbuf, rbuf) of (None, b) \<Rightarrow> return [] | (Some sb_ptr, None) \<Rightarrow> return [] | (Some sb_ptr, Some rb_ptr) \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [length msg_registers + 1..<Suc (unat n)];
return $ min n $ nat_to_len $ length hardware_mrs + length buf_mrs
od \<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\<rbrace> do hardware_mrs <- return $ take (unat n) msg_registers;
mapM (\<lambda>r. do v <- as_user sender $ getRegister r;
as_user receiver $ setRegister r v
od) hardware_mrs;
buf_mrs <- case (sbuf, rbuf) of (None, b) \<Rightarrow> return [] | (Some sb_ptr, None) \<Rightarrow> return [] | (Some sb_ptr, Some rb_ptr) \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [length msg_registers + 1..<Suc (unat n)];
return $ min n $ nat_to_len $ length hardware_mrs + length buf_mrs
od \<lbrace>\<lambda>_. pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state\<rbrace> proof (prove)
goal:
No subgoals!