theory Ipc_AC

lemma transfer_caps_integrity_autarch:
  "\<lbrace>pas_refined aag and integrity aag X st and valid_objs and valid_mdb and
    (\<lambda>s. (\<forall>x\<in>set caps. s \<turnstile> fst x) \<and>
         (\<forall>x\<in>set caps. 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> ipc_buffer_has_auth aag receiver receive_buffer \<and>
       (\<forall>x\<in>set caps. is_subject aag (fst (snd x))) \<and> length caps < 6)\<rbrace>
   transfer_caps mi caps endpoint receiver receive_buffer
   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: transfer_caps_def) apply (wpc | wp)+ apply (rule_tac P = "\<forall>x \<in> set dest_slots. is_subject aag (fst x)" in hoare_gen_asm) apply (wp transfer_caps_loop_pres_dest cap_insert_integrity_autarch
              set_extra_badge_integrity_autarch[where thread=receiver]
              get_receive_slots_authorised hoare_vcg_all_lift hoare_vcg_imp_lift
           | simp add: msg_align_bits' buffer_cptr_index_def
                       msg_max_length_def cte_wp_at_caps_of_state
           | blast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and integrity aag X st and valid_objs and valid_mdb and (\<lambda>s. (\<forall>x\<in>set caps. s \<turnstile> fst x) \<and> (\<forall>x\<in>set caps. 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> ipc_buffer_has_auth aag receiver receive_buffer \<and> (\<forall>x\<in>set caps. is_subject aag (fst (snd x))) \<and> length caps < 6)\<rbrace> transfer_caps mi caps endpoint receiver receive_buffer \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver receive_buffer \<and> (\<forall>x\<in>set caps. is_subject aag (fst (snd x))) \<and> length caps < 6 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and valid_objs and valid_mdb and (\<lambda>s. (\<forall>x\<in>set caps. s \<turnstile> fst x) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s))\<rbrace> transfer_caps mi caps endpoint receiver receive_buffer \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver receive_buffer \<and> (\<forall>x\<in>set caps. is_subject aag (fst (snd x))) \<and> length caps < 6 \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and valid_objs and valid_mdb and (\<lambda>s. (\<forall>x\<in>set caps. s \<turnstile> fst x) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s))\<rbrace> do dest_slots <- get_receive_slots receiver receive_buffer;
case receive_buffer of None \<Rightarrow> return (MI (mi_length mi) 0 0 (mi_label mi)) | Some receive_buffer \<Rightarrow> transfer_caps_loop endpoint receive_buffer 0 caps dest_slots (MI (mi_length mi) 0 0 (mi_label mi))
od \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>dest_slots x2. \<lbrakk>is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver receive_buffer \<and> (\<forall>x\<in>set caps. is_subject aag (fst (snd x))) \<and> length caps < 6; receive_buffer = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R13 dest_slots x2\<rbrace> transfer_caps_loop endpoint x2 0 caps dest_slots (MI (mi_length mi) 0 0 (mi_label mi)) \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 2. is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver receive_buffer \<and> (\<forall>x\<in>set caps. is_subject aag (fst (snd x))) \<and> length caps < 6 \<Longrightarrow> \<lbrace>?Q2\<rbrace> get_receive_slots receiver receive_buffer \<lbrace>\<lambda>dest_slots s. (receive_buffer = None \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. receive_buffer = Some x \<longrightarrow> ?R13 dest_slots x s)\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver receive_buffer \<and> (\<forall>x\<in>set caps. is_subject aag (fst (snd x))) \<and> length caps < 6; (pas_refined aag and integrity aag X st and valid_objs and valid_mdb and (\<lambda>s. (\<forall>x\<in>set caps. s \<turnstile> fst x) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s))) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>dest_slots x2. \<lbrakk>is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver receive_buffer \<and> (\<forall>x\<in>set caps. is_subject aag (fst (snd x))) \<and> length caps < 6; receive_buffer = Some x2; \<forall>x\<in>set dest_slots. is_subject aag (fst x)\<rbrakk> \<Longrightarrow> \<lbrace>?P'18 dest_slots x2\<rbrace> transfer_caps_loop endpoint x2 0 caps dest_slots (MI (mi_length mi) 0 0 (mi_label mi)) \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>
 2. is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver receive_buffer \<and> (\<forall>x\<in>set caps. is_subject aag (fst (snd x))) \<and> length caps < 6 \<Longrightarrow> \<lbrace>?Q2\<rbrace> get_receive_slots receiver receive_buffer \<lbrace>\<lambda>dest_slots s. (receive_buffer = None \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. receive_buffer = Some x \<longrightarrow> (?P'18 dest_slots x and K (\<forall>x\<in>set dest_slots. is_subject aag (fst x))) s)\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag receiver \<and> ipc_buffer_has_auth aag receiver receive_buffer \<and> (\<forall>x\<in>set caps. is_subject aag (fst (snd x))) \<and> length caps < 6; (pas_refined aag and integrity aag X st and valid_objs and valid_mdb and (\<lambda>s. (\<forall>x\<in>set caps. s \<turnstile> fst x) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s))) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal:
No subgoals!