theory Ipc_AC

lemma transfer_caps_loop_pas_refined:
  "\<lbrace>\<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and>
        valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and>
        (\<forall>x \<in> set caps. valid_cap (fst x) s \<and> real_cte_at (snd x) s
                      \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s) \<and>
        (\<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) \<and>
        (\<forall>slot \<in> set slots. is_subject aag (fst slot)) \<and>
        (\<forall>x \<in> set caps. is_subject aag (fst (snd x)) \<and>
        pas_cap_cur_auth aag (fst x)) \<and> distinct slots\<rbrace>
   transfer_caps_loop ep buffer n caps slots mi
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (rule hoare_pre) apply (rule transfer_caps_loop_presM_extended
              [where vo=True and em=True and ex=False and
                     Psrc="\<lambda>slot . is_subject aag (fst slot)" and
                     Pcap="pas_cap_cur_auth aag" and
                     Pdest="\<lambda>slot . is_subject aag (fst slot)"]) apply (wp cap_insert_pas_refined) apply (fastforce simp: cte_wp_at_caps_of_state elim!: is_derived_is_transferable) apply (rule set_extra_badge_pas_refined) apply (erule(1) auth_derived_pas_cur_auth) apply (fastforce elim: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s) \<and> (\<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot)) \<and> (\<forall>x\<in>set caps. is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x)) \<and> distinct slots\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s) \<and> (\<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot)) \<and> (\<forall>x\<in>set caps. is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x)) \<and> distinct slots \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>cap src dest. \<lbrace>\<lambda>s. pas_refined aag s \<and> (True \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> real_cte_at dest s \<and> s \<turnstile> cap \<and> is_subject aag (fst src) \<and> is_subject aag (fst dest) \<and> pas_cap_cur_auth aag cap \<and> tcb_cap_valid cap dest s \<and> real_cte_at src s \<and> cte_wp_at (is_derived (cdt s) src cap) src s \<and> cap \<noteq> NullCap) \<and> (True \<longrightarrow> cte_wp_at ((=) NullCap) dest s) \<and> (False \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>b n. \<lbrace>pas_refined aag\<rbrace> set_extra_badge buffer b n \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. \<And>cap cap'. \<lbrakk>auth_derived cap cap'; pas_cap_cur_auth aag cap'\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag cap
 4. \<And>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s) \<and> (\<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot)) \<and> (\<forall>x\<in>set caps. is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x)) \<and> distinct slots \<Longrightarrow> pas_refined aag s \<and> (True \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s \<and> is_subject aag (fst x)) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x) \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal (4 subgoals):
 1. \<And>cap src dest s. pas_refined aag s \<and> (True \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> real_cte_at dest s \<and> s \<turnstile> cap \<and> is_subject aag (fst src) \<and> is_subject aag (fst dest) \<and> pas_cap_cur_auth aag cap \<and> tcb_cap_valid cap dest s \<and> real_cte_at src s \<and> cte_wp_at (is_derived (cdt s) src cap) src s \<and> cap \<noteq> NullCap) \<and> (True \<longrightarrow> cte_wp_at ((=) NullCap) dest s) \<and> (False \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s) \<Longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and (\<lambda>s. is_transferable_in src s \<and> \<not> Option.is_none (cdt s src) \<longrightarrow> is_transferable_cap cap) and K (is_subject aag (fst dest) \<and> is_subject aag (fst src) \<and> pas_cap_cur_auth aag cap)) s
 2. \<And>b n. \<lbrace>pas_refined aag\<rbrace> set_extra_badge buffer b n \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. \<And>cap cap'. \<lbrakk>auth_derived cap cap'; pas_cap_cur_auth aag cap'\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag cap
 4. \<And>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s) \<and> (\<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot)) \<and> (\<forall>x\<in>set caps. is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x)) \<and> distinct slots \<Longrightarrow> pas_refined aag s \<and> (True \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s \<and> is_subject aag (fst x)) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x) \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal (3 subgoals):
 1. \<And>b n. \<lbrace>pas_refined aag\<rbrace> set_extra_badge buffer b n \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>cap cap'. \<lbrakk>auth_derived cap cap'; pas_cap_cur_auth aag cap'\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag cap
 3. \<And>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s) \<and> (\<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot)) \<and> (\<forall>x\<in>set caps. is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x)) \<and> distinct slots \<Longrightarrow> pas_refined aag s \<and> (True \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s \<and> is_subject aag (fst x)) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x) \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal (2 subgoals):
 1. \<And>cap cap'. \<lbrakk>auth_derived cap cap'; pas_cap_cur_auth aag cap'\<rbrakk> \<Longrightarrow> pas_cap_cur_auth aag cap
 2. \<And>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s) \<and> (\<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot)) \<and> (\<forall>x\<in>set caps. is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x)) \<and> distinct slots \<Longrightarrow> pas_refined aag s \<and> (True \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s \<and> is_subject aag (fst x)) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x) \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s) \<and> (\<forall>x\<in>set slots. real_cte_at x s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) x s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot)) \<and> (\<forall>x\<in>set caps. is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x)) \<and> distinct slots \<Longrightarrow> pas_refined aag s \<and> (True \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s \<and> is_subject aag (fst x)) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> is_subject aag (fst (snd x)) \<and> pas_cap_cur_auth aag (fst x) \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal:
No subgoals!