theory Ipc_AC

lemma transfer_caps_loop_respects_in_ipc_autarch:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and valid_objs and valid_mdb and
    (\<lambda>s. (\<forall>slot \<in> set slots. real_cte_at slot 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
    K ((\<forall>cap \<in> set caps. is_subject aag (fst (snd cap))) \<and>
       (\<forall>slot \<in> set slots. is_subject aag (fst slot)) \<and>
       (\<not> is_subject aag receiver
        \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buffer msg_align_bits) \<and>
            is_aligned buffer msg_align_bits \<and> n + length caps < 6 \<and> distinct slots)\<rbrace>
   transfer_caps_loop ep buffer n caps slots mi
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" apply (rule hoare_gen_asm) apply (wp transfer_caps_loop_pres_dest cap_inserintegrity_in_ipc_autarch
         | simp add: msg_align_bits' buffer_cptr_index_def msg_max_length_def
         | blast)+ apply (auto simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and valid_objs and valid_mdb and (\<lambda>s. (\<forall>slot\<in>set slots. real_cte_at slot 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 K ((\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot)) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buffer msg_align_bits) \<and> is_aligned buffer msg_align_bits \<and> n + length caps < 6 \<and> distinct slots)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot)) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buffer msg_align_bits) \<and> is_aligned buffer msg_align_bits \<and> n + length caps < 6 \<and> distinct slots \<Longrightarrow> \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and valid_objs and valid_mdb and (\<lambda>s. (\<forall>slot\<in>set slots. real_cte_at slot 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))\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>(\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot)) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range buffer (word_size_bits + 7)) \<and> is_aligned buffer (word_size_bits + 7) \<and> n + length caps < 6 \<and> distinct slots; integrity_tcb_in_ipc aag X receiver epptr TRContext st s \<and> valid_objs s \<and> valid_mdb s \<and> (\<forall>slot\<in>set slots. real_cte_at slot 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)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s proof (prove)
goal:
No subgoals!