theory Ipc_DR

lemma transfer_caps_dcorres:
  "dcorres dc \<top>
           (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node
            and valid_objs and pspace_aligned
            and pspace_distinct and valid_mdb
            and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some rcv_buffer \<and>
             (\<forall>x\<in>set caps. (\<lambda>(cap, slot).  real_cte_at slot s \<and> valid_cap cap s \<and>
                 cte_wp_at (\<lambda>cp'. (cap \<noteq> cap.NullCap \<longrightarrow> cp'\<noteq>cap \<longrightarrow> cp' = masked_as_full cap cap )) slot s) x)
                 \<and> 2 + msg_max_length + length caps < max_ipc_length) and valid_etcbs)
           (Endpoint_D.transfer_caps ep
              (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)
              sender rcv)
           (Ipc_A.transfer_caps info caps ep rcv rcv_buffer)" unfolding Ipc_A.transfer_caps_def Endpoint_D.transfer_caps_def apply clarsimp apply (cases rcv_buffer) apply simp apply (rule corres_dummy_return_r) apply (rule corres_guard_imp) apply (rule corres_split[where r'="\<lambda>r r'. r = None" and P=\<top> and P'=\<top>]) apply (rule corres_alternate2) apply simp apply simp apply (rule transfer_caps_loop_None) apply wp+ apply simp apply simp apply (simp del: get_receive_slots.simps) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule corres_alternate1) apply (rule get_receive_slot_dcorres) apply (unfold dc_def)[1] apply (rule dcorres_transfer_caps_loop, auto)[1] apply wp[1] apply (simp only: ball_conj_distrib) apply (wp get_rs_cte_at) apply simp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some rcv_buffer \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> 2 + msg_max_length + length caps < max_ipc_length) and valid_etcbs) (Endpoint_D.transfer_caps ep (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps) sender rcv) (Ipc_A.transfer_caps info caps ep rcv rcv_buffer) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some rcv_buffer \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> 2 + msg_max_length + length caps < max_ipc_length) and valid_etcbs) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (do dest_slots <- get_receive_slots rcv rcv_buffer;
mi' <- return $ MI (mi_length info) 0 0 (mi_label info);
case rcv_buffer of None \<Rightarrow> return mi' | Some receive_buffer \<Rightarrow> Ipc_A.transfer_caps_loop ep receive_buffer 0 caps dest_slots mi'
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some rcv_buffer \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (do dest_slots <- get_receive_slots rcv rcv_buffer;
case rcv_buffer of None \<Rightarrow> return (MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> Ipc_A.transfer_caps_loop ep receive_buffer 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info))
od) proof (prove)
goal (2 subgoals):
 1. rcv_buffer = None \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some rcv_buffer \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (do dest_slots <- get_receive_slots rcv rcv_buffer;
case rcv_buffer of None \<Rightarrow> return (MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> Ipc_A.transfer_caps_loop ep receive_buffer 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info))
od)
 2. \<And>a. rcv_buffer = Some a \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some rcv_buffer \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (do dest_slots <- get_receive_slots rcv rcv_buffer;
case rcv_buffer of None \<Rightarrow> return (MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> Ipc_A.transfer_caps_loop ep receive_buffer 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info))
od) proof (prove)
goal (2 subgoals):
 1. rcv_buffer = None \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some None \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (return (MI (mi_length info) 0 0 (mi_label info)))
 2. \<And>a. rcv_buffer = Some a \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some rcv_buffer \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (do dest_slots <- get_receive_slots rcv rcv_buffer;
case rcv_buffer of None \<Rightarrow> return (MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> Ipc_A.transfer_caps_loop ep receive_buffer 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info))
od) proof (prove)
goal (2 subgoals):
 1. rcv_buffer = None \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some None \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (return (MI (mi_length info) 0 0 (mi_label info)) >>= return)
 2. \<And>a. rcv_buffer = Some a \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some rcv_buffer \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (do dest_slots <- get_receive_slots rcv rcv_buffer;
case rcv_buffer of None \<Rightarrow> return (MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> Ipc_A.transfer_caps_loop ep receive_buffer 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info))
od) proof (prove)
goal (4 subgoals):
 1. rcv_buffer = None \<Longrightarrow> dcorres dc ?Q4 ?Q'4 ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (return (MI (mi_length info) 0 0 (mi_label info)) >>= return)
 2. \<And>s. \<lbrakk>rcv_buffer = None; True\<rbrakk> \<Longrightarrow> ?Q4 s
 3. \<And>s. \<lbrakk>rcv_buffer = None; (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some None \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'4 s
 4. \<And>a. rcv_buffer = Some a \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some rcv_buffer \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (do dest_slots <- get_receive_slots rcv rcv_buffer;
case rcv_buffer of None \<Rightarrow> return (MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> Ipc_A.transfer_caps_loop ep receive_buffer 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info))
od) proof (prove)
goal (7 subgoals):
 1. rcv_buffer = None \<Longrightarrow> dcorres (\<lambda>r r'. r = None) (\<lambda>_. True) (\<lambda>_. True) (get_receive_slot rcv \<sqinter> return None) (return (MI (mi_length info) 0 0 (mi_label info)))
 2. \<And>dest_slot x. \<lbrakk>rcv_buffer = None; dest_slot = None\<rbrakk> \<Longrightarrow> dcorres dc (?R8 dest_slot) (?R'8 x) (Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps) dest_slot) (return x)
 3. rcv_buffer = None \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_receive_slot rcv \<sqinter> return None \<lbrace>?R8\<rbrace>
 4. rcv_buffer = None \<Longrightarrow> \<lbrace>?Q'8\<rbrace> return (MI (mi_length info) 0 0 (mi_label info)) \<lbrace>?R'8\<rbrace>
 5. \<And>s. \<lbrakk>rcv_buffer = None; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 6. \<And>s. \<lbrakk>rcv_buffer = None; (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some None \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s
 7. \<And>a. rcv_buffer = Some a \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some rcv_buffer \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (do dest_slots <- get_receive_slots rcv rcv_buffer;
case rcv_buffer of None \<Rightarrow> return (MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> Ipc_A.transfer_caps_loop ep receive_buffer 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info))
od) proof (prove)
goal (7 subgoals):
 1. rcv_buffer = None \<Longrightarrow> dcorres (\<lambda>r r'. r = None) (\<lambda>_. True) (\<lambda>_. True) (return None) (return (MI (mi_length info) 0 0 (mi_label info)))
 2. \<And>dest_slot x. \<lbrakk>rcv_buffer = None; dest_slot = None\<rbrakk> \<Longrightarrow> dcorres dc (?R8 dest_slot) (?R'8 x) (Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps) dest_slot) (return x)
 3. rcv_buffer = None \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_receive_slot rcv \<sqinter> return None \<lbrace>?R8\<rbrace>
 4. rcv_buffer = None \<Longrightarrow> \<lbrace>?Q'8\<rbrace> return (MI (mi_length info) 0 0 (mi_label info)) \<lbrace>?R'8\<rbrace>
 5. \<And>s. \<lbrakk>rcv_buffer = None; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 6. \<And>s. \<lbrakk>rcv_buffer = None; (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some None \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s
 7. \<And>a. rcv_buffer = Some a \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some rcv_buffer \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (do dest_slots <- get_receive_slots rcv rcv_buffer;
case rcv_buffer of None \<Rightarrow> return (MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> Ipc_A.transfer_caps_loop ep receive_buffer 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info))
od) proof (prove)
goal (6 subgoals):
 1. \<And>dest_slot x. \<lbrakk>rcv_buffer = None; dest_slot = None\<rbrakk> \<Longrightarrow> dcorres dc (?R8 dest_slot) (?R'8 x) (Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps) dest_slot) (return x)
 2. rcv_buffer = None \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_receive_slot rcv \<sqinter> return None \<lbrace>?R8\<rbrace>
 3. rcv_buffer = None \<Longrightarrow> \<lbrace>?Q'8\<rbrace> return (MI (mi_length info) 0 0 (mi_label info)) \<lbrace>?R'8\<rbrace>
 4. \<And>s. \<lbrakk>rcv_buffer = None; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 5. \<And>s. \<lbrakk>rcv_buffer = None; (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some None \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s
 6. \<And>a. rcv_buffer = Some a \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some rcv_buffer \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (do dest_slots <- get_receive_slots rcv rcv_buffer;
case rcv_buffer of None \<Rightarrow> return (MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> Ipc_A.transfer_caps_loop ep receive_buffer 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info))
od) proof (prove)
goal (6 subgoals):
 1. \<And>dest_slot x. \<lbrakk>rcv_buffer = None; dest_slot = None\<rbrakk> \<Longrightarrow> dcorres dc (?R8 None) (?R'8 x) (Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps) None) (return x)
 2. rcv_buffer = None \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_receive_slot rcv \<sqinter> return None \<lbrace>?R8\<rbrace>
 3. rcv_buffer = None \<Longrightarrow> \<lbrace>?Q'8\<rbrace> return (MI (mi_length info) 0 0 (mi_label info)) \<lbrace>?R'8\<rbrace>
 4. \<And>s. \<lbrakk>rcv_buffer = None; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 5. \<And>s. \<lbrakk>rcv_buffer = None; (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some None \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s
 6. \<And>a. rcv_buffer = Some a \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some rcv_buffer \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (do dest_slots <- get_receive_slots rcv rcv_buffer;
case rcv_buffer of None \<Rightarrow> return (MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> Ipc_A.transfer_caps_loop ep receive_buffer 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info))
od) proof (prove)
goal (5 subgoals):
 1. rcv_buffer = None \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_receive_slot rcv \<sqinter> return None \<lbrace>\<lambda>a b. True\<rbrace>
 2. rcv_buffer = None \<Longrightarrow> \<lbrace>?Q'8\<rbrace> return (MI (mi_length info) 0 0 (mi_label info)) \<lbrace>\<lambda>a. tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs\<rbrace>
 3. \<And>s. \<lbrakk>rcv_buffer = None; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 4. \<And>s. \<lbrakk>rcv_buffer = None; (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some None \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'8) s
 5. \<And>a. rcv_buffer = Some a \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some rcv_buffer \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (do dest_slots <- get_receive_slots rcv rcv_buffer;
case rcv_buffer of None \<Rightarrow> return (MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> Ipc_A.transfer_caps_loop ep receive_buffer 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info))
od) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>rcv_buffer = None; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ((\<lambda>_. True) and (\<lambda>a. True))) s
 2. \<And>s. \<lbrakk>rcv_buffer = None; (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some None \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs)) s
 3. \<And>a. rcv_buffer = Some a \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some rcv_buffer \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (do dest_slots <- get_receive_slots rcv rcv_buffer;
case rcv_buffer of None \<Rightarrow> return (MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> Ipc_A.transfer_caps_loop ep receive_buffer 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info))
od) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>rcv_buffer = None; (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some None \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_etcbs)) s
 2. \<And>a. rcv_buffer = Some a \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some rcv_buffer \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (do dest_slots <- get_receive_slots rcv rcv_buffer;
case rcv_buffer of None \<Rightarrow> return (MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> Ipc_A.transfer_caps_loop ep receive_buffer 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info))
od) proof (prove)
goal (1 subgoal):
 1. \<And>a. rcv_buffer = Some a \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some rcv_buffer \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (do dest_slots <- get_receive_slots rcv rcv_buffer;
case rcv_buffer of None \<Rightarrow> return (MI (mi_length info) 0 0 (mi_label info)) | Some receive_buffer \<Rightarrow> Ipc_A.transfer_caps_loop ep receive_buffer 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info))
od) proof (prove)
goal (1 subgoal):
 1. \<And>a. rcv_buffer = Some a \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a) \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (do dest_slots <- get_receive_slots rcv (Some a);
Ipc_A.transfer_caps_loop ep a 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info))
od) proof (prove)
goal (3 subgoals):
 1. \<And>a. rcv_buffer = Some a \<Longrightarrow> dcorres dc (?Q25 a) (?Q'25 a) ((get_receive_slot rcv \<sqinter> return None) >>= Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps)) (do dest_slots <- get_receive_slots rcv (Some a);
Ipc_A.transfer_caps_loop ep a 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info))
od)
 2. \<And>a s. \<lbrakk>rcv_buffer = Some a; True\<rbrakk> \<Longrightarrow> ?Q25 a s
 3. \<And>a s. \<lbrakk>rcv_buffer = Some a; (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a) \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'25 a s proof (prove)
goal (6 subgoals):
 1. \<And>a. rcv_buffer = Some a \<Longrightarrow> dcorres (?r'29 a) (?P29 a) (?P'29 a) (get_receive_slot rcv \<sqinter> return None) (get_receive_slots rcv (Some a))
 2. \<And>a dest_slot dest_slots. \<lbrakk>rcv_buffer = Some a; ?r'29 a dest_slot dest_slots\<rbrakk> \<Longrightarrow> dcorres dc (?R29 a dest_slot) (?R'29 a dest_slots) (Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps) dest_slot) (Ipc_A.transfer_caps_loop ep a 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info)))
 3. \<And>a. rcv_buffer = Some a \<Longrightarrow> \<lbrace>?Q29 a\<rbrace> get_receive_slot rcv \<sqinter> return None \<lbrace>?R29 a\<rbrace>
 4. \<And>a. rcv_buffer = Some a \<Longrightarrow> \<lbrace>?Q'29 a\<rbrace> get_receive_slots rcv (Some a) \<lbrace>?R'29 a\<rbrace>
 5. \<And>a s. \<lbrakk>rcv_buffer = Some a; True\<rbrakk> \<Longrightarrow> (?P29 a and ?Q29 a) s
 6. \<And>a s. \<lbrakk>rcv_buffer = Some a; (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a) \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'29 a and ?Q'29 a) s proof (prove)
goal (6 subgoals):
 1. \<And>a. rcv_buffer = Some a \<Longrightarrow> dcorres (?r'29 a) (?P29 a) (?P'29 a) (get_receive_slot rcv) (get_receive_slots rcv (Some a))
 2. \<And>a dest_slot dest_slots. \<lbrakk>rcv_buffer = Some a; ?r'29 a dest_slot dest_slots\<rbrakk> \<Longrightarrow> dcorres dc (?R29 a dest_slot) (?R'29 a dest_slots) (Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps) dest_slot) (Ipc_A.transfer_caps_loop ep a 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info)))
 3. \<And>a. rcv_buffer = Some a \<Longrightarrow> \<lbrace>?Q29 a\<rbrace> get_receive_slot rcv \<sqinter> return None \<lbrace>?R29 a\<rbrace>
 4. \<And>a. rcv_buffer = Some a \<Longrightarrow> \<lbrace>?Q'29 a\<rbrace> get_receive_slots rcv (Some a) \<lbrace>?R'29 a\<rbrace>
 5. \<And>a s. \<lbrakk>rcv_buffer = Some a; True\<rbrakk> \<Longrightarrow> (?P29 a and ?Q29 a) s
 6. \<And>a s. \<lbrakk>rcv_buffer = Some a; (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a) \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'29 a and ?Q'29 a) s proof (prove)
goal (5 subgoals):
 1. \<And>a dest_slot dest_slots. \<lbrakk>rcv_buffer = Some a; dest_slot = dest_of dest_slots\<rbrakk> \<Longrightarrow> dcorres dc (?R29 a dest_slot) (?R'29 a dest_slots) (Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps) dest_slot) (Ipc_A.transfer_caps_loop ep a 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info)))
 2. \<And>a. rcv_buffer = Some a \<Longrightarrow> \<lbrace>?Q29 a\<rbrace> get_receive_slot rcv \<sqinter> return None \<lbrace>?R29 a\<rbrace>
 3. \<And>a. rcv_buffer = Some a \<Longrightarrow> \<lbrace>?Q'29 a\<rbrace> get_receive_slots rcv (Some a) \<lbrace>?R'29 a\<rbrace>
 4. \<And>a s. \<lbrakk>rcv_buffer = Some a; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q29 a) s
 5. \<And>a s. \<lbrakk>rcv_buffer = Some a; (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a) \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a)) and not_idle_thread rcv and valid_objs and valid_global_refs and valid_irq_node and valid_idle and not_idle_thread rcv and valid_etcbs and ?Q'29 a) s proof (prove)
goal (5 subgoals):
 1. \<And>a dest_slot dest_slots. \<lbrakk>rcv_buffer = Some a; dest_slot = dest_of dest_slots\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. True) (?R29 a dest_slot) (?R'29 a dest_slots) (Endpoint_D.transfer_caps_loop ep rcv (map (\<lambda>(cap, slot). (transform_cap cap, transform_cslot_ptr slot)) caps) dest_slot) (Ipc_A.transfer_caps_loop ep a 0 caps dest_slots (MI (mi_length info) 0 0 (mi_label info)))
 2. \<And>a. rcv_buffer = Some a \<Longrightarrow> \<lbrace>?Q29 a\<rbrace> get_receive_slot rcv \<sqinter> return None \<lbrace>?R29 a\<rbrace>
 3. \<And>a. rcv_buffer = Some a \<Longrightarrow> \<lbrace>?Q'29 a\<rbrace> get_receive_slots rcv (Some a) \<lbrace>?R'29 a\<rbrace>
 4. \<And>a s. \<lbrakk>rcv_buffer = Some a; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q29 a) s
 5. \<And>a s. \<lbrakk>rcv_buffer = Some a; (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a) \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a)) and not_idle_thread rcv and valid_objs and valid_global_refs and valid_irq_node and valid_idle and not_idle_thread rcv and valid_etcbs and ?Q'29 a) s proof (prove)
goal (4 subgoals):
 1. \<And>a. rcv_buffer = Some a \<Longrightarrow> \<lbrace>?Q29 a\<rbrace> get_receive_slot rcv \<sqinter> return None \<lbrace>\<lambda>dest_slot _. True\<rbrace>
 2. \<And>a. rcv_buffer = Some a \<Longrightarrow> \<lbrace>?Q'29 a\<rbrace> get_receive_slots rcv (Some a) \<lbrace>\<lambda>dest_slots. valid_idle and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a)) and not_idle_thread rcv and (\<lambda>s. (\<forall>x\<in>set dest_slots. cte_wp_at (\<lambda>cap. cap = cap.NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>(cap, slot)\<in>set caps. real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> length dest_slots \<le> 1 \<and> 2 + msg_max_length + 0 + length caps < max_ipc_length) and valid_etcbs\<rbrace>
 3. \<And>a s. \<lbrakk>rcv_buffer = Some a; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q29 a) s
 4. \<And>a s. \<lbrakk>rcv_buffer = Some a; (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a) \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a)) and not_idle_thread rcv and valid_objs and valid_global_refs and valid_irq_node and valid_idle and not_idle_thread rcv and valid_etcbs and ?Q'29 a) s proof (prove)
goal (3 subgoals):
 1. \<And>a. rcv_buffer = Some a \<Longrightarrow> \<lbrace>?Q'29 a\<rbrace> get_receive_slots rcv (Some a) \<lbrace>\<lambda>dest_slots. valid_idle and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a)) and not_idle_thread rcv and (\<lambda>s. (\<forall>x\<in>set dest_slots. cte_wp_at (\<lambda>cap. cap = cap.NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>(cap, slot)\<in>set caps. real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> length dest_slots \<le> 1 \<and> 2 + msg_max_length + 0 + length caps < max_ipc_length) and valid_etcbs\<rbrace>
 2. \<And>a s. \<lbrakk>rcv_buffer = Some a; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ((\<lambda>_. True) and (\<lambda>a. True))) s
 3. \<And>a s. \<lbrakk>rcv_buffer = Some a; (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a) \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a)) and not_idle_thread rcv and valid_objs and valid_global_refs and valid_irq_node and valid_idle and not_idle_thread rcv and valid_etcbs and ?Q'29 a) s proof (prove)
goal (3 subgoals):
 1. \<And>a. rcv_buffer = Some a \<Longrightarrow> \<lbrace>?Q'29 a\<rbrace> get_receive_slots rcv (Some a) \<lbrace>\<lambda>dest_slots. valid_idle and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a)) and not_idle_thread rcv and (\<lambda>s. ((\<forall>x\<in>set dest_slots. cte_wp_at (\<lambda>cap. cap = cap.NullCap) x s) \<and> (\<forall>x\<in>set dest_slots. real_cte_at x s)) \<and> (\<forall>(cap, slot)\<in>set caps. real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> length dest_slots \<le> 1 \<and> 2 + msg_max_length + 0 + length caps < max_ipc_length) and valid_etcbs\<rbrace>
 2. \<And>a s. \<lbrakk>rcv_buffer = Some a; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ((\<lambda>_. True) and (\<lambda>a. True))) s
 3. \<And>a s. \<lbrakk>rcv_buffer = Some a; (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a) \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a)) and not_idle_thread rcv and valid_objs and valid_global_refs and valid_irq_node and valid_idle and not_idle_thread rcv and valid_etcbs and ?Q'29 a) s proof (prove)
goal (2 subgoals):
 1. \<And>a s. \<lbrakk>rcv_buffer = Some a; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ((\<lambda>_. True) and (\<lambda>a. True))) s
 2. \<And>a s. \<lbrakk>rcv_buffer = Some a; (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a) \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a)) and not_idle_thread rcv and valid_objs and valid_global_refs and valid_irq_node and valid_idle and not_idle_thread rcv and valid_etcbs and (\<lambda>s. (valid_idle and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a)) and not_idle_thread rcv) s \<and> True \<and> valid_objs s \<and> (\<forall>(cap, slot)\<in>set caps. real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> True \<and> 2 + msg_max_length + 0 + length caps < max_ipc_length \<and> valid_etcbs s)) s proof (prove)
goal (1 subgoal):
 1. \<And>a s. \<lbrakk>rcv_buffer = Some a; (tcb_at rcv and valid_idle and not_idle_thread rcv and valid_global_refs and valid_irq_node and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a) \<and> (\<forall>x\<in>set caps. case x of (cap, slot) \<Rightarrow> real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> Suc (Suc (msg_max_length + length caps)) < max_ipc_length) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a)) and not_idle_thread rcv and valid_objs and valid_global_refs and valid_irq_node and valid_idle and not_idle_thread rcv and valid_etcbs and (\<lambda>s. (valid_idle and valid_objs and pspace_aligned and pspace_distinct and valid_mdb and (\<lambda>s. evalMonad (lookup_ipc_buffer True rcv) s = Some (Some a)) and not_idle_thread rcv) s \<and> True \<and> valid_objs s \<and> (\<forall>(cap, slot)\<in>set caps. real_cte_at slot s \<and> s \<turnstile> cap \<and> cte_wp_at (\<lambda>cp'. cap \<noteq> cap.NullCap \<longrightarrow> cp' \<noteq> cap \<longrightarrow> cp' = masked_as_full cap cap) slot s) \<and> True \<and> 2 + msg_max_length + 0 + length caps < max_ipc_length \<and> valid_etcbs s)) s proof (prove)
goal:
No subgoals!