theory Ipc_AC

lemma get_receive_slots_authorised:
  "\<lbrace>pas_refined aag and K (\<forall>rbuf. recv_buf = Some rbuf \<longrightarrow> is_subject aag receiver)\<rbrace>
   get_receive_slots receiver recv_buf
   \<lbrace>\<lambda>rv _. \<forall>slot \<in> set rv. is_subject aag (fst slot)\<rbrace>" apply (rule hoare_gen_asm) apply (cases recv_buf) apply (simp, wp, simp) apply clarsimp apply (wp get_cap_auth_wp[where aag=aag] lookup_slot_for_thread_authorised
         | rule hoare_drop_imps
         | simp add: lookup_cap_def split_def)+ apply (strengthen cnode_cap_all_auth_owns, simp add: aag_cap_auth_def) apply (wp hoare_vcg_all_lift_R hoare_drop_imps)+ apply clarsimp apply (fastforce simp: is_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (\<forall>rbuf. recv_buf = Some rbuf \<longrightarrow> is_subject aag receiver)\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv _. \<forall>slot\<in>set rv. is_subject aag (fst slot)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>rbuf. recv_buf = Some rbuf \<longrightarrow> is_subject aag receiver \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv _. \<forall>slot\<in>set rv. is_subject aag (fst slot)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>rbuf. recv_buf = Some rbuf \<longrightarrow> is_subject aag receiver; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv _. \<forall>slot\<in>set rv. is_subject aag (fst slot)\<rbrace>
 2. \<And>a. \<lbrakk>\<forall>rbuf. recv_buf = Some rbuf \<longrightarrow> is_subject aag receiver; recv_buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv _. \<forall>slot\<in>set rv. is_subject aag (fst slot)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<forall>rbuf. recv_buf = Some rbuf \<longrightarrow> is_subject aag receiver; recv_buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> get_receive_slots receiver recv_buf \<lbrace>\<lambda>rv _. \<forall>slot\<in>set rv. is_subject aag (fst slot)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>is_subject aag receiver; recv_buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> do ct <- load_cap_transfer a;
empty_on_failure (doE cnode <- unify_failure (lookup_cap receiver (ct_receive_root ct));
slot <- unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct)));
cap <- liftE (get_cap slot);
y <- whenE (cap \<noteq> NullCap) (throwError ());
returnOk [slot]
odE)
od \<lbrace>\<lambda>rv _. \<forall>slot\<in>set rv. is_subject aag (fst slot)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>a ct. \<lbrakk>is_subject aag receiver; recv_buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?P'77 a ct\<rbrace> lookup_slot_for_thread receiver (ct_receive_root ct) \<lbrace>\<lambda>rv s. \<forall>cap. caps_of_state s (fst rv) = Some cap \<and> pas_cap_cur_auth aag cap \<longrightarrow> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x)) \<and> pas_refined aag s \<and> (is_cnode_cap cap \<longrightarrow> (\<forall>x\<in>obj_refs_ac cap. is_subject aag x))\<rbrace>, -
 2. \<And>a. \<lbrakk>is_subject aag receiver; recv_buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a\<rbrace> load_cap_transfer a \<lbrace>\<lambda>ct s. (\<forall>slot\<in>set []. is_subject aag (fst slot)) \<and> True \<and> True \<and> True \<and> pas_refined aag s \<and> pas_refined aag s \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag receiver)) s \<and> ?P'77 a ct s\<rbrace>
 3. \<And>a s. \<lbrakk>is_subject aag receiver; recv_buf = Some a; pas_refined aag s\<rbrakk> \<Longrightarrow> ?Q7 a s proof (prove)
goal (3 subgoals):
 1. \<And>a ct. \<lbrakk>is_subject aag receiver; recv_buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?P'77 a ct\<rbrace> lookup_slot_for_thread receiver (ct_receive_root ct) \<lbrace>\<lambda>r s. \<forall>x. caps_of_state s (fst r) = Some x \<and> (\<forall>xa\<in>obj_refs_ac x. \<forall>auth\<in>cap_auth_conferred x. (pasSubject aag, auth, pasObjectAbs aag xa) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range x. (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) x \<and> cap_links_irq aag (pasSubject aag) x \<longrightarrow> (is_cnode_cap x \<longrightarrow> (\<exists>s. pas_refined aag s)) \<and> pas_refined aag s \<and> (is_cnode_cap x \<longrightarrow> (\<exists>s. pas_refined aag s))\<rbrace>, -
 2. \<And>a. \<lbrakk>is_subject aag receiver; recv_buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a\<rbrace> load_cap_transfer a \<lbrace>\<lambda>ct s. (\<forall>slot\<in>set []. is_subject aag (fst slot)) \<and> True \<and> True \<and> True \<and> pas_refined aag s \<and> pas_refined aag s \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag receiver)) s \<and> ?P'77 a ct s\<rbrace>
 3. \<And>a s. \<lbrakk>is_subject aag receiver; recv_buf = Some a; pas_refined aag s\<rbrakk> \<Longrightarrow> ?Q7 a s proof (prove)
goal (1 subgoal):
 1. \<And>a s. \<lbrakk>is_subject aag receiver; recv_buf = Some a; pas_refined aag s\<rbrakk> \<Longrightarrow> (\<forall>slot\<in>set []. is_subject aag (fst slot)) \<and> True \<and> True \<and> True \<and> pas_refined aag s \<and> pas_refined aag s \<and> True \<and> pas_refined aag s \<and> (pas_refined aag and K (is_subject aag receiver)) s \<and> (\<forall>x. (\<exists>s. pas_refined aag s) \<and> pas_refined aag s \<and> (\<exists>s. pas_refined aag s)) proof (prove)
goal (1 subgoal):
 1. \<And>a s. \<lbrakk>is_subject aag receiver; recv_buf = Some a; pas_refined aag s\<rbrakk> \<Longrightarrow> Ex (pas_refined aag) proof (prove)
goal:
No subgoals!