theory Ipc_AC

lemma transfer_caps_respects_in_ipc:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and
    pas_refined aag and valid_objs and valid_mdb and tcb_at receiver 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 ((\<not> null caps \<longrightarrow> is_subject aag receiver) \<and> length caps < 6 \<and>
                        (\<forall>cap \<in> set caps. is_subject aag (fst (snd cap))) \<and>
                        (\<not> is_subject aag receiver \<longrightarrow>
                         case_option True (\<lambda>buf'. auth_ipc_buffers st receiver =
                                                  ptr_range buf' msg_align_bits) recv_buf) \<and>
                        (case_option True (\<lambda>buf'. is_aligned buf' msg_align_bits) recv_buf))\<rbrace>
   transfer_caps mi caps endpoint receiver recv_buf
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" apply (rule hoare_gen_asm) apply (cases recv_buf) apply (simp add: transfer_caps_def, wp, simp) apply (cases caps) apply (simp add: transfer_caps_def del: get_receive_slots.simps, wp, simp) apply (simp add: transfer_caps_def del: get_receive_slots.simps) apply (wp transfer_caps_loop_respects_in_ipc_autarch get_receive_slots_authorised
         | wpc | rule hoare_drop_imps | simp add: null_def del: get_receive_slots.simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and pas_refined aag and valid_objs and valid_mdb and tcb_at receiver 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 ((\<not> null caps \<longrightarrow> is_subject aag receiver) \<and> length caps < 6 \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))\<rbrace> transfer_caps mi caps endpoint receiver recv_buf \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<not> null caps \<longrightarrow> is_subject aag receiver) \<and> length caps < 6 \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits) \<Longrightarrow> \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and pas_refined aag and valid_objs and valid_mdb and tcb_at receiver 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 recv_buf \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<not> null caps \<longrightarrow> is_subject aag receiver) \<and> length caps < 6 \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and pas_refined aag and valid_objs and valid_mdb and tcb_at receiver 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 recv_buf \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>
 2. \<And>a. \<lbrakk>(\<not> null caps \<longrightarrow> is_subject aag receiver) \<and> length caps < 6 \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); recv_buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and pas_refined aag and valid_objs and valid_mdb and tcb_at receiver 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 recv_buf \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>(\<not> null caps \<longrightarrow> is_subject aag receiver) \<and> length caps < 6 \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); recv_buf = Some a\<rbrakk> \<Longrightarrow> \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and pas_refined aag and valid_objs and valid_mdb and tcb_at receiver 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 recv_buf \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>(\<not> null caps \<longrightarrow> is_subject aag receiver) \<and> length caps < 6 \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); recv_buf = Some a; caps = []\<rbrakk> \<Longrightarrow> \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and pas_refined aag and valid_objs and valid_mdb and tcb_at receiver 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 recv_buf \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>
 2. \<And>a aa list. \<lbrakk>(\<not> null caps \<longrightarrow> is_subject aag receiver) \<and> length caps < 6 \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); recv_buf = Some a; caps = aa # list\<rbrakk> \<Longrightarrow> \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and pas_refined aag and valid_objs and valid_mdb and tcb_at receiver 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 recv_buf \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a aa list. \<lbrakk>(\<not> null caps \<longrightarrow> is_subject aag receiver) \<and> length caps < 6 \<and> (\<forall>cap\<in>set caps. is_subject aag (fst (snd cap))) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> auth_ipc_buffers st receiver = ptr_range buf' msg_align_bits)) \<and> (case recv_buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits); recv_buf = Some a; caps = aa # list\<rbrakk> \<Longrightarrow> \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and pas_refined aag and valid_objs and valid_mdb and tcb_at receiver 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 recv_buf \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a aa list. \<lbrakk>(\<not> null (aa # list) \<longrightarrow> is_subject aag receiver) \<and> length list < 5 \<and> is_subject aag (fst (snd aa)) \<and> (\<forall>cap\<in>set list. is_subject aag (fst (snd cap))) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> auth_ipc_buffers st receiver = ptr_range a msg_align_bits) \<and> is_aligned a msg_align_bits; recv_buf = Some a; caps = aa # list\<rbrakk> \<Longrightarrow> \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and pas_refined aag and valid_objs and valid_mdb and tcb_at receiver and (\<lambda>s. s \<turnstile> fst aa \<and> (\<forall>x\<in>set list. s \<turnstile> fst x) \<and> cte_wp_at (\<lambda>cp. fst aa \<noteq> NullCap \<longrightarrow> cp = fst aa) (snd aa) s \<and> real_cte_at (snd aa) s \<and> (\<forall>x\<in>set list. 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 (Some a);
transfer_caps_loop endpoint a 0 (aa # list) dest_slots (MI (mi_length mi) 0 0 (mi_label mi))
od \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal:
No subgoals!