theory Ipc_R

lemma getReceiveSlots_corres:
  "corres (\<lambda>xs ys. ys = map cte_map xs)
    (tcb_at receiver and valid_objs and pspace_aligned)
    (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and
     case_option \<top> valid_ipc_buffer_ptr' recv_buf)
    (get_receive_slots receiver recv_buf)
    (getReceiveSlots receiver recv_buf)" apply (cases recv_buf) apply (simp add: getReceiveSlots_def) apply (simp add: getReceiveSlots_def split_def) apply (rule corres_guard_imp) apply (rule corres_split[OF loadCapTransfer_corres]) apply (rule corres_empty_on_failure) apply (rule corres_splitEE) apply (rule corres_unify_failure) apply (rule lookup_cap_corres) apply (simp add: ct_relation_def) apply simp apply (rule corres_splitEE) apply (rule corres_unify_failure) apply (simp add: ct_relation_def) apply (erule lookupSlotForCNodeOp_corres [OF _ refl]) apply simp apply (simp add: split_def liftE_bindE unlessE_whenE) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split_norE) apply (rule corres_whenE) apply (case_tac cap, auto)[1] apply (rule corres_trivial, simp) apply simp apply (rule corres_trivial, simp add: returnOk_def) apply (wp lookup_cap_valid lookup_cap_valid' lsfco_cte_at | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>xs ys. ys = map cte_map xs) (tcb_at receiver and valid_objs and pspace_aligned) (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (get_receive_slots receiver recv_buf) (getReceiveSlots receiver recv_buf) proof (prove)
goal (2 subgoals):
 1. recv_buf = None \<Longrightarrow> corres (\<lambda>xs ys. ys = map cte_map xs) (tcb_at receiver and valid_objs and pspace_aligned) (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (get_receive_slots receiver recv_buf) (getReceiveSlots receiver recv_buf)
 2. \<And>a. recv_buf = Some a \<Longrightarrow> corres (\<lambda>xs ys. ys = map cte_map xs) (tcb_at receiver and valid_objs and pspace_aligned) (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (get_receive_slots receiver recv_buf) (getReceiveSlots receiver recv_buf) proof (prove)
goal (1 subgoal):
 1. \<And>a. recv_buf = Some a \<Longrightarrow> corres (\<lambda>xs ys. ys = map cte_map xs) (tcb_at receiver and valid_objs and pspace_aligned) (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (get_receive_slots receiver recv_buf) (getReceiveSlots receiver recv_buf) proof (prove)
goal (1 subgoal):
 1. \<And>a. recv_buf = Some a \<Longrightarrow> corres (\<lambda>xs ys. ys = map cte_map xs) (tcb_at receiver and valid_objs and pspace_aligned) (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and valid_ipc_buffer_ptr' a) (do ct <- load_cap_transfer a;
empty_on_failure (doE cnode <- unify_failure (lookup_cap receiver (ct_receive_root ct));
slot <- unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct)));
cap <- liftE (get_cap slot);
y <- whenE (cap \<noteq> cap.NullCap) (throwError ());
returnOk [slot]
odE)
od) (do ct <- loadCapTransfer a;
emptyOnFailure (doE cnode <- unifyFailure (lookupCap receiver (ctReceiveRoot ct));
slot <- unifyFailure (lookupSlotForCNodeOp False cnode (ctReceiveIndex ct) (ctReceiveDepth ct));
cte <- liftE (getCTE slot);
y <- unlessE (cteCap cte = capability.NullCap) (throwError ());
returnOk [slot]
odE)
od) proof (prove)
goal (3 subgoals):
 1. \<And>a. recv_buf = Some a \<Longrightarrow> corres (\<lambda>xs ys. ys = map cte_map xs) (?Q6 a) (?Q'6 a) (do ct <- load_cap_transfer a;
empty_on_failure (doE cnode <- unify_failure (lookup_cap receiver (ct_receive_root ct));
slot <- unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct)));
cap <- liftE (get_cap slot);
y <- whenE (cap \<noteq> cap.NullCap) (throwError ());
returnOk [slot]
odE)
od) (do ct <- loadCapTransfer a;
emptyOnFailure (doE cnode <- unifyFailure (lookupCap receiver (ctReceiveRoot ct));
slot <- unifyFailure (lookupSlotForCNodeOp False cnode (ctReceiveIndex ct) (ctReceiveDepth ct));
cte <- liftE (getCTE slot);
y <- unlessE (cteCap cte = capability.NullCap) (throwError ());
returnOk [slot]
odE)
od)
 2. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at receiver and valid_objs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ?Q6 a s
 3. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> ?Q'6 a s proof (prove)
goal (5 subgoals):
 1. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> corres (\<lambda>xs ys. ys = map cte_map xs) (?R10 a ct) (?R'10 a cta) (empty_on_failure (doE cnode <- unify_failure (lookup_cap receiver (ct_receive_root ct));
slot <- unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct)));
cap <- liftE (get_cap slot);
y <- whenE (cap \<noteq> cap.NullCap) (throwError ());
returnOk [slot]
odE)) (emptyOnFailure (doE cnode <- unifyFailure (lookupCap receiver (ctReceiveRoot cta));
slot <- unifyFailure (lookupSlotForCNodeOp False cnode (ctReceiveIndex cta) (ctReceiveDepth cta));
cte <- liftE (getCTE slot);
y <- unlessE (cteCap cte = capability.NullCap) (throwError ());
returnOk [slot]
odE))
 2. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q10 a\<rbrace> load_cap_transfer a \<lbrace>?R10 a\<rbrace>
 3. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q'10 a\<rbrace> loadCapTransfer a \<lbrace>?R'10 a\<rbrace>
 4. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at receiver and valid_objs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a) s
 5. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_ipc_buffer_ptr' a and ?Q'10 a) s proof (prove)
goal (5 subgoals):
 1. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. [] = map cte_map []) \<oplus> (\<lambda>xs ys. ys = map cte_map xs)) (?R10 a ct) (?R'10 a cta) (doE cnode <- unify_failure (lookup_cap receiver (ct_receive_root ct));
slot <- unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct)));
cap <- liftE (get_cap slot);
y <- whenE (cap \<noteq> cap.NullCap) (throwError ());
returnOk [slot]
odE) (doE cnode <- unifyFailure (lookupCap receiver (ctReceiveRoot cta));
slot <- unifyFailure (lookupSlotForCNodeOp False cnode (ctReceiveIndex cta) (ctReceiveDepth cta));
cte <- liftE (getCTE slot);
y <- unlessE (cteCap cte = capability.NullCap) (throwError ());
returnOk [slot]
odE)
 2. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q10 a\<rbrace> load_cap_transfer a \<lbrace>?R10 a\<rbrace>
 3. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q'10 a\<rbrace> loadCapTransfer a \<lbrace>?R'10 a\<rbrace>
 4. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at receiver and valid_objs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a) s
 5. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_ipc_buffer_ptr' a and ?Q'10 a) s proof (prove)
goal (8 subgoals):
 1. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. [] = map cte_map []) \<oplus> ?r'17 a ct cta) (?P18 a ct) (?P'20 a cta) (unify_failure (lookup_cap receiver (ct_receive_root ct))) (unifyFailure (lookupCap receiver (ctReceiveRoot cta)))
 2. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; ?r'17 a ct cta cnode cnodea\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. [] = map cte_map []) \<oplus> (\<lambda>xs ys. ys = map cte_map xs)) (?R17 a ct cta cnode) (?R'17 a ct cta cnodea) (doE slot <- unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct)));
cap <- liftE (get_cap slot);
y <- whenE (cap \<noteq> cap.NullCap) (throwError ());
returnOk [slot]
odE) (doE slot <- unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta));
cte <- liftE (getCTE slot);
y <- unlessE (cteCap cte = capability.NullCap) (throwError ());
returnOk [slot]
odE)
 3. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a ct\<rbrace> unify_failure (lookup_cap receiver (ct_receive_root ct)) \<lbrace>?R17 a ct cta\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 a cta\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot cta)) \<lbrace>?R'17 a ct cta\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q10 a\<rbrace> load_cap_transfer a \<lbrace>\<lambda>ct. ?P18 a ct and ?Q19 a ct\<rbrace>
 6. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q'10 a\<rbrace> loadCapTransfer a \<lbrace>\<lambda>cta. ?P'20 a cta and ?Q'21 a cta\<rbrace>
 7. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at receiver and valid_objs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a) s
 8. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_ipc_buffer_ptr' a and ?Q'10 a) s proof (prove)
goal (9 subgoals):
 1. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> corres (?f'26 a ct cta \<oplus> ?r'17 a ct cta) (?P18 a ct) (?P'20 a cta) (lookup_cap receiver (ct_receive_root ct)) (lookupCap receiver (ctReceiveRoot cta))
 2. \<And>a ct cta ft ft'. \<lbrakk>recv_buf = Some a; ct_relation ct cta; ?f'26 a ct cta ft ft'\<rbrakk> \<Longrightarrow> [] = map cte_map []
 3. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; ?r'17 a ct cta cnode cnodea\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. [] = map cte_map []) \<oplus> (\<lambda>xs ys. ys = map cte_map xs)) (?R17 a ct cta cnode) (?R'17 a ct cta cnodea) (doE slot <- unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct)));
cap <- liftE (get_cap slot);
y <- whenE (cap \<noteq> cap.NullCap) (throwError ());
returnOk [slot]
odE) (doE slot <- unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta));
cte <- liftE (getCTE slot);
y <- unlessE (cteCap cte = capability.NullCap) (throwError ());
returnOk [slot]
odE)
 4. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a ct\<rbrace> unify_failure (lookup_cap receiver (ct_receive_root ct)) \<lbrace>?R17 a ct cta\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 a cta\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot cta)) \<lbrace>?R'17 a ct cta\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q10 a\<rbrace> load_cap_transfer a \<lbrace>\<lambda>ct. ?P18 a ct and ?Q19 a ct\<rbrace>
 7. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q'10 a\<rbrace> loadCapTransfer a \<lbrace>\<lambda>cta. ?P'20 a cta and ?Q'21 a cta\<rbrace>
 8. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at receiver and valid_objs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a) s
 9. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_ipc_buffer_ptr' a and ?Q'10 a) s proof (prove)
goal (9 subgoals):
 1. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> ct_receive_root ct = to_bl (ctReceiveRoot cta)
 2. \<And>a ct cta ft ft'. \<lbrakk>recv_buf = Some a; ct_relation ct cta; lfr ft ft'\<rbrakk> \<Longrightarrow> [] = map cte_map []
 3. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. [] = map cte_map []) \<oplus> (\<lambda>xs ys. ys = map cte_map xs)) (?R17 a ct cta cnode) (?R'17 a ct cta cnodea) (doE slot <- unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct)));
cap <- liftE (get_cap slot);
y <- whenE (cap \<noteq> cap.NullCap) (throwError ());
returnOk [slot]
odE) (doE slot <- unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta));
cte <- liftE (getCTE slot);
y <- unlessE (cteCap cte = capability.NullCap) (throwError ());
returnOk [slot]
odE)
 4. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a ct\<rbrace> unify_failure (lookup_cap receiver (ct_receive_root ct)) \<lbrace>?R17 a ct cta\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 a cta\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot cta)) \<lbrace>?R'17 a ct cta\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q10 a\<rbrace> load_cap_transfer a \<lbrace>\<lambda>ct. valid_objs and pspace_aligned and tcb_at receiver and ?Q19 a ct\<rbrace>
 7. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q'10 a\<rbrace> loadCapTransfer a \<lbrace>\<lambda>cta. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' receiver and ?Q'21 a cta\<rbrace>
 8. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at receiver and valid_objs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a) s
 9. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_ipc_buffer_ptr' a and ?Q'10 a) s proof (prove)
goal (8 subgoals):
 1. \<And>a ct cta ft ft'. \<lbrakk>recv_buf = Some a; ct_relation ct cta; lfr ft ft'\<rbrakk> \<Longrightarrow> [] = map cte_map []
 2. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. [] = map cte_map []) \<oplus> (\<lambda>xs ys. ys = map cte_map xs)) (?R17 a ct cta cnode) (?R'17 a ct cta cnodea) (doE slot <- unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct)));
cap <- liftE (get_cap slot);
y <- whenE (cap \<noteq> cap.NullCap) (throwError ());
returnOk [slot]
odE) (doE slot <- unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta));
cte <- liftE (getCTE slot);
y <- unlessE (cteCap cte = capability.NullCap) (throwError ());
returnOk [slot]
odE)
 3. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a ct\<rbrace> unify_failure (lookup_cap receiver (ct_receive_root ct)) \<lbrace>?R17 a ct cta\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 a cta\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot cta)) \<lbrace>?R'17 a ct cta\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q10 a\<rbrace> load_cap_transfer a \<lbrace>\<lambda>ct. valid_objs and pspace_aligned and tcb_at receiver and ?Q19 a ct\<rbrace>
 6. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q'10 a\<rbrace> loadCapTransfer a \<lbrace>\<lambda>cta. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' receiver and ?Q'21 a cta\<rbrace>
 7. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at receiver and valid_objs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a) s
 8. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_ipc_buffer_ptr' a and ?Q'10 a) s proof (prove)
goal (7 subgoals):
 1. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. [] = map cte_map []) \<oplus> (\<lambda>xs ys. ys = map cte_map xs)) (?R17 a ct cta cnode) (?R'17 a ct cta cnodea) (doE slot <- unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct)));
cap <- liftE (get_cap slot);
y <- whenE (cap \<noteq> cap.NullCap) (throwError ());
returnOk [slot]
odE) (doE slot <- unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta));
cte <- liftE (getCTE slot);
y <- unlessE (cteCap cte = capability.NullCap) (throwError ());
returnOk [slot]
odE)
 2. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a ct\<rbrace> unify_failure (lookup_cap receiver (ct_receive_root ct)) \<lbrace>?R17 a ct cta\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 a cta\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot cta)) \<lbrace>?R'17 a ct cta\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q10 a\<rbrace> load_cap_transfer a \<lbrace>\<lambda>ct. valid_objs and pspace_aligned and tcb_at receiver and ?Q19 a ct\<rbrace>
 5. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q'10 a\<rbrace> loadCapTransfer a \<lbrace>\<lambda>cta. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' receiver and ?Q'21 a cta\<rbrace>
 6. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at receiver and valid_objs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a) s
 7. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_ipc_buffer_ptr' a and ?Q'10 a) s proof (prove)
goal (10 subgoals):
 1. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. [] = map cte_map []) \<oplus> ?r'33 a ct cta cnode cnodea) (?P34 a ct cta cnode) (?P'36 a ct cta cnodea) (unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct)))) (unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta)))
 2. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; ?r'33 a ct cta cnode cnodea slot slota\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. [] = map cte_map []) \<oplus> (\<lambda>xs ys. ys = map cte_map xs)) (?R33 a ct cta cnode cnodea slot) (?R'33 a ct cta cnode cnodea slota) (doE cap <- liftE (get_cap slot);
y <- whenE (cap \<noteq> cap.NullCap) (throwError ());
returnOk [slot]
odE) (doE cte <- liftE (getCTE slota);
y <- unlessE (cteCap cte = capability.NullCap) (throwError ());
returnOk [slota]
odE)
 3. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a ct cta cnode\<rbrace> unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct))) \<lbrace>?R33 a ct cta cnode cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 a ct cta cnodea\<rbrace> unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta)) \<lbrace>?R'33 a ct cta cnode cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a ct\<rbrace> unify_failure (lookup_cap receiver (ct_receive_root ct)) \<lbrace>\<lambda>cnode. ?P34 a ct cta cnode and ?Q35 a ct cta cnode\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 a cta\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot cta)) \<lbrace>\<lambda>cnodea. ?P'36 a ct cta cnodea and ?Q'37 a ct cta cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q10 a\<rbrace> load_cap_transfer a \<lbrace>\<lambda>ct. valid_objs and pspace_aligned and tcb_at receiver and ?Q19 a ct\<rbrace>
 8. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q'10 a\<rbrace> loadCapTransfer a \<lbrace>\<lambda>cta. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' receiver and ?Q'21 a cta\<rbrace>
 9. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at receiver and valid_objs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a) s
 10. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_ipc_buffer_ptr' a and ?Q'10 a) s proof (prove)
goal (11 subgoals):
 1. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> corres (?f'42 a ct cta cnode cnodea \<oplus> ?r'33 a ct cta cnode cnodea) (?P34 a ct cta cnode) (?P'36 a ct cta cnodea) (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct))) (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta))
 2. \<And>a ct cta cnode cnodea ft ft'. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; ?f'42 a ct cta cnode cnodea ft ft'\<rbrakk> \<Longrightarrow> [] = map cte_map []
 3. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; ?r'33 a ct cta cnode cnodea slot slota\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. [] = map cte_map []) \<oplus> (\<lambda>xs ys. ys = map cte_map xs)) (?R33 a ct cta cnode cnodea slot) (?R'33 a ct cta cnode cnodea slota) (doE cap <- liftE (get_cap slot);
y <- whenE (cap \<noteq> cap.NullCap) (throwError ());
returnOk [slot]
odE) (doE cte <- liftE (getCTE slota);
y <- unlessE (cteCap cte = capability.NullCap) (throwError ());
returnOk [slota]
odE)
 4. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a ct cta cnode\<rbrace> unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct))) \<lbrace>?R33 a ct cta cnode cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 a ct cta cnodea\<rbrace> unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta)) \<lbrace>?R'33 a ct cta cnode cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a ct\<rbrace> unify_failure (lookup_cap receiver (ct_receive_root ct)) \<lbrace>\<lambda>cnode. ?P34 a ct cta cnode and ?Q35 a ct cta cnode\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 a cta\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot cta)) \<lbrace>\<lambda>cnodea. ?P'36 a ct cta cnodea and ?Q'37 a ct cta cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q10 a\<rbrace> load_cap_transfer a \<lbrace>\<lambda>ct. valid_objs and pspace_aligned and tcb_at receiver and ?Q19 a ct\<rbrace>
 9. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q'10 a\<rbrace> loadCapTransfer a \<lbrace>\<lambda>cta. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' receiver and ?Q'21 a cta\<rbrace>
 10. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at receiver and valid_objs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_receive_root ct = to_bl (ctReceiveRoot cta) \<and> ct_receive_index ct = to_bl (ctReceiveIndex cta) \<and> ctReceiveDepth cta = unat (ct_receive_depth ct); cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> corres (?f'42 a ct cta cnode cnodea \<oplus> ?r'33 a ct cta cnode cnodea) (?P34 a ct cta cnode) (?P'36 a ct cta cnodea) (lookup_slot_for_cnode_op False cnode (to_bl (ctReceiveIndex cta)) (unat (ct_receive_depth ct))) (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (unat (ct_receive_depth ct)))
 2. \<And>a ct cta cnode cnodea ft ft'. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; ?f'42 a ct cta cnode cnodea ft ft'\<rbrakk> \<Longrightarrow> [] = map cte_map []
 3. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; ?r'33 a ct cta cnode cnodea slot slota\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. [] = map cte_map []) \<oplus> (\<lambda>xs ys. ys = map cte_map xs)) (?R33 a ct cta cnode cnodea slot) (?R'33 a ct cta cnode cnodea slota) (doE cap <- liftE (get_cap slot);
y <- whenE (cap \<noteq> cap.NullCap) (throwError ());
returnOk [slot]
odE) (doE cte <- liftE (getCTE slota);
y <- unlessE (cteCap cte = capability.NullCap) (throwError ());
returnOk [slota]
odE)
 4. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a ct cta cnode\<rbrace> unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct))) \<lbrace>?R33 a ct cta cnode cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 a ct cta cnodea\<rbrace> unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta)) \<lbrace>?R'33 a ct cta cnode cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a ct\<rbrace> unify_failure (lookup_cap receiver (ct_receive_root ct)) \<lbrace>\<lambda>cnode. ?P34 a ct cta cnode and ?Q35 a ct cta cnode\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 a cta\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot cta)) \<lbrace>\<lambda>cnodea. ?P'36 a ct cta cnodea and ?Q'37 a ct cta cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q10 a\<rbrace> load_cap_transfer a \<lbrace>\<lambda>ct. valid_objs and pspace_aligned and tcb_at receiver and ?Q19 a ct\<rbrace>
 9. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q'10 a\<rbrace> loadCapTransfer a \<lbrace>\<lambda>cta. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' receiver and ?Q'21 a cta\<rbrace>
 10. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at receiver and valid_objs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>a ct cta cnode cnodea ft ft'. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; ser ft ft'\<rbrakk> \<Longrightarrow> [] = map cte_map []
 2. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. [] = map cte_map []) \<oplus> (\<lambda>xs ys. ys = map cte_map xs)) (?R33 a ct cta cnode cnodea slot) (?R'33 a ct cta cnode cnodea slota) (doE cap <- liftE (get_cap slot);
y <- whenE (cap \<noteq> cap.NullCap) (throwError ());
returnOk [slot]
odE) (doE cte <- liftE (getCTE slota);
y <- unlessE (cteCap cte = capability.NullCap) (throwError ());
returnOk [slota]
odE)
 3. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a ct cta cnode\<rbrace> unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct))) \<lbrace>?R33 a ct cta cnode cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 a ct cta cnodea\<rbrace> unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta)) \<lbrace>?R'33 a ct cta cnode cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a ct\<rbrace> unify_failure (lookup_cap receiver (ct_receive_root ct)) \<lbrace>\<lambda>cnode. valid_objs and pspace_aligned and valid_cap cnode and ?Q35 a ct cta cnode\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 a cta\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot cta)) \<lbrace>\<lambda>cnodea. valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' cnodea and ?Q'37 a ct cta cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q10 a\<rbrace> load_cap_transfer a \<lbrace>\<lambda>ct. valid_objs and pspace_aligned and tcb_at receiver and ?Q19 a ct\<rbrace>
 8. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q'10 a\<rbrace> loadCapTransfer a \<lbrace>\<lambda>cta. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' receiver and ?Q'21 a cta\<rbrace>
 9. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at receiver and valid_objs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a) s
 10. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_ipc_buffer_ptr' a and ?Q'10 a) s proof (prove)
goal (9 subgoals):
 1. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. [] = map cte_map []) \<oplus> (\<lambda>xs ys. ys = map cte_map xs)) (?R33 a ct cta cnode cnodea slot) (?R'33 a ct cta cnode cnodea slota) (doE cap <- liftE (get_cap slot);
y <- whenE (cap \<noteq> cap.NullCap) (throwError ());
returnOk [slot]
odE) (doE cte <- liftE (getCTE slota);
y <- unlessE (cteCap cte = capability.NullCap) (throwError ());
returnOk [slota]
odE)
 2. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a ct cta cnode\<rbrace> unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct))) \<lbrace>?R33 a ct cta cnode cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 a ct cta cnodea\<rbrace> unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta)) \<lbrace>?R'33 a ct cta cnode cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a ct\<rbrace> unify_failure (lookup_cap receiver (ct_receive_root ct)) \<lbrace>\<lambda>cnode. valid_objs and pspace_aligned and valid_cap cnode and ?Q35 a ct cta cnode\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 a cta\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot cta)) \<lbrace>\<lambda>cnodea. valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' cnodea and ?Q'37 a ct cta cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q10 a\<rbrace> load_cap_transfer a \<lbrace>\<lambda>ct. valid_objs and pspace_aligned and tcb_at receiver and ?Q19 a ct\<rbrace>
 7. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q'10 a\<rbrace> loadCapTransfer a \<lbrace>\<lambda>cta. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' receiver and ?Q'21 a cta\<rbrace>
 8. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at receiver and valid_objs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a) s
 9. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_ipc_buffer_ptr' a and ?Q'10 a) s proof (prove)
goal (9 subgoals):
 1. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. True) \<oplus> (\<lambda>xs ys. ys = map cte_map xs)) (?R33 a ct cta cnode cnodea slot) (?R'33 a ct cta cnode cnodea (cte_map slot)) (do cap <- get_cap slot;
doE y <- whenE (cap \<noteq> cap.NullCap) (throwError ());
returnOk [slot]
odE
od) (do cte <- getCTE (cte_map slot);
doE y <- whenE (cteCap cte \<noteq> capability.NullCap) (throwError ());
returnOk [cte_map slot]
odE
od)
 2. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a ct cta cnode\<rbrace> unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct))) \<lbrace>?R33 a ct cta cnode cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 a ct cta cnodea\<rbrace> unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta)) \<lbrace>?R'33 a ct cta cnode cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a ct\<rbrace> unify_failure (lookup_cap receiver (ct_receive_root ct)) \<lbrace>\<lambda>cnode. valid_objs and pspace_aligned and valid_cap cnode and ?Q35 a ct cta cnode\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 a cta\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot cta)) \<lbrace>\<lambda>cnodea. valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' cnodea and ?Q'37 a ct cta cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q10 a\<rbrace> load_cap_transfer a \<lbrace>\<lambda>ct. valid_objs and pspace_aligned and tcb_at receiver and ?Q19 a ct\<rbrace>
 7. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q'10 a\<rbrace> loadCapTransfer a \<lbrace>\<lambda>cta. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' receiver and ?Q'21 a cta\<rbrace>
 8. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at receiver and valid_objs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a) s
 9. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at' receiver and valid_objs' and pspace_aligned' and pspace_distinct' and valid_ipc_buffer_ptr' a) s\<rbrakk> \<Longrightarrow> (valid_ipc_buffer_ptr' a and ?Q'10 a) s proof (prove)
goal (11 subgoals):
 1. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. True) \<oplus> (\<lambda>xs ys. ys = map cte_map xs)) (?R48 a ct cta cnode cnodea slot slota cap) (?R'48 a ct cta cnode cnodea slot slota cte) (doE y <- whenE (cap \<noteq> cap.NullCap) (throwError ());
returnOk [slot]
odE) (doE y <- whenE (cteCap cte \<noteq> capability.NullCap) (throwError ());
returnOk [cte_map slot]
odE)
 2. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q55 a ct cta cnode cnodea slot\<rbrace> get_cap slot \<lbrace>?R48 a ct cta cnode cnodea slot slota\<rbrace>
 3. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 a ct cta cnode cnodea (cte_map slot)\<rbrace> getCTE (cte_map slot) \<lbrace>?R'48 a ct cta cnode cnodea slot slota\<rbrace>
 4. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a ct cta cnode\<rbrace> unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct))) \<lbrace>\<lambda>b. cte_wp_at (\<lambda>_. True) b and ?Q55 a ct cta cnode cnodea b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 a ct cta cnodea\<rbrace> unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta)) \<lbrace>\<lambda>b. pspace_aligned' and pspace_distinct' and ?Q'52 a ct cta cnode cnodea b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a ct\<rbrace> unify_failure (lookup_cap receiver (ct_receive_root ct)) \<lbrace>\<lambda>cnode. valid_objs and pspace_aligned and valid_cap cnode and ?Q35 a ct cta cnode\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 a cta\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot cta)) \<lbrace>\<lambda>cnodea. valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' cnodea and ?Q'37 a ct cta cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q10 a\<rbrace> load_cap_transfer a \<lbrace>\<lambda>ct. valid_objs and pspace_aligned and tcb_at receiver and ?Q19 a ct\<rbrace>
 9. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q'10 a\<rbrace> loadCapTransfer a \<lbrace>\<lambda>cta. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' receiver and ?Q'21 a cta\<rbrace>
 10. \<And>a s. \<lbrakk>recv_buf = Some a; (tcb_at receiver and valid_objs and pspace_aligned) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q10 a) s
A total of 11 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. True) \<oplus> dc) (?P60 a ct cta cnode cnodea slot slota cap) (?P'62 a ct cta cnode cnodea slot slota cte) (whenE (cap \<noteq> cap.NullCap) (throwError ())) (whenE (cteCap cte \<noteq> capability.NullCap) (throwError ()))
 2. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. True) \<oplus> (\<lambda>xs ys. ys = map cte_map xs)) (?R59 a ct cta cnode cnodea slot slota cap cte) (?R'59 a ct cta cnode cnodea slot slota cap cte) (returnOk [slot]) (returnOk [cte_map slot])
 3. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> \<lbrace>?Q61 a ct cta cnode cnodea slot slota cap\<rbrace> whenE (cap \<noteq> cap.NullCap) (throwError ()) \<lbrace>\<lambda>x. ?R59 a ct cta cnode cnodea slot slota cap cte\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'63 a ct cta cnode cnodea slot slota cte\<rbrace> whenE (cteCap cte \<noteq> capability.NullCap) (throwError ()) \<lbrace>\<lambda>x. ?R'59 a ct cta cnode cnodea slot slota cap cte\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q55 a ct cta cnode cnodea slot\<rbrace> get_cap slot \<lbrace>\<lambda>cap. ?P60 a ct cta cnode cnodea slot slota cap and ?Q61 a ct cta cnode cnodea slot slota cap\<rbrace>
 6. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 a ct cta cnode cnodea (cte_map slot)\<rbrace> getCTE (cte_map slot) \<lbrace>\<lambda>cte. ?P'62 a ct cta cnode cnodea slot slota cte and ?Q'63 a ct cta cnode cnodea slot slota cte\<rbrace>
 7. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a ct cta cnode\<rbrace> unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct))) \<lbrace>\<lambda>b. cte_wp_at (\<lambda>_. True) b and ?Q55 a ct cta cnode cnodea b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 a ct cta cnodea\<rbrace> unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta)) \<lbrace>\<lambda>b. pspace_aligned' and pspace_distinct' and ?Q'52 a ct cta cnode cnodea b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a ct\<rbrace> unify_failure (lookup_cap receiver (ct_receive_root ct)) \<lbrace>\<lambda>cnode. valid_objs and pspace_aligned and valid_cap cnode and ?Q35 a ct cta cnode\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 a cta\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot cta)) \<lbrace>\<lambda>cnodea. valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' cnodea and ?Q'37 a ct cta cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 14 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> (cap \<noteq> cap.NullCap) = (cteCap cte \<noteq> capability.NullCap)
 2. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. True) \<oplus> dc) (?P70 a ct cta cnode cnodea slot slota cap) (?P'72 a ct cta cnode cnodea slot slota cte) (throwError ()) (throwError ())
 3. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> dc () ()
 4. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. True) \<oplus> (\<lambda>xs ys. ys = map cte_map xs)) (?R59 a ct cta cnode cnodea slot slota cap cte) (?R'59 a ct cta cnode cnodea slot slota cap cte) (returnOk [slot]) (returnOk [cte_map slot])
 5. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> \<lbrace>?Q61 a ct cta cnode cnodea slot slota cap\<rbrace> whenE (cap \<noteq> cap.NullCap) (throwError ()) \<lbrace>\<lambda>x. ?R59 a ct cta cnode cnodea slot slota cap cte\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'63 a ct cta cnode cnodea slot slota cte\<rbrace> whenE (cteCap cte \<noteq> capability.NullCap) (throwError ()) \<lbrace>\<lambda>x. ?R'59 a ct cta cnode cnodea slot slota cap cte\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q55 a ct cta cnode cnodea slot\<rbrace> get_cap slot \<lbrace>\<lambda>cap. (\<lambda>s. cap \<noteq> cap.NullCap \<longrightarrow> ?P70 a ct cta cnode cnodea slot slota cap s) and ?Q61 a ct cta cnode cnodea slot slota cap\<rbrace>
 8. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 a ct cta cnode cnodea (cte_map slot)\<rbrace> getCTE (cte_map slot) \<lbrace>\<lambda>cte. (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?P'72 a ct cta cnode cnodea slot slota cte s) and ?Q'63 a ct cta cnode cnodea slot slota cte\<rbrace>
 9. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a ct cta cnode\<rbrace> unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct))) \<lbrace>\<lambda>b. cte_wp_at (\<lambda>_. True) b and ?Q55 a ct cta cnode cnodea b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 a ct cta cnodea\<rbrace> unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta)) \<lbrace>\<lambda>b. pspace_aligned' and pspace_distinct' and ?Q'52 a ct cta cnode cnodea b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. True) \<oplus> dc) (?P70 a ct cta cnode cnodea slot slota cap) (?P'72 a ct cta cnode cnodea slot slota cte) (throwError ()) (throwError ())
 2. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> dc () ()
 3. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. True) \<oplus> (\<lambda>xs ys. ys = map cte_map xs)) (?R59 a ct cta cnode cnodea slot slota cap cte) (?R'59 a ct cta cnode cnodea slot slota cap cte) (returnOk [slot]) (returnOk [cte_map slot])
 4. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> \<lbrace>?Q61 a ct cta cnode cnodea slot slota cap\<rbrace> whenE (cap \<noteq> cap.NullCap) (throwError ()) \<lbrace>\<lambda>x. ?R59 a ct cta cnode cnodea slot slota cap cte\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'63 a ct cta cnode cnodea slot slota cte\<rbrace> whenE (cteCap cte \<noteq> capability.NullCap) (throwError ()) \<lbrace>\<lambda>x. ?R'59 a ct cta cnode cnodea slot slota cap cte\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q55 a ct cta cnode cnodea slot\<rbrace> get_cap slot \<lbrace>\<lambda>cap. (\<lambda>s. cap \<noteq> cap.NullCap \<longrightarrow> ?P70 a ct cta cnode cnodea slot slota cap s) and ?Q61 a ct cta cnode cnodea slot slota cap\<rbrace>
 7. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 a ct cta cnode cnodea (cte_map slot)\<rbrace> getCTE (cte_map slot) \<lbrace>\<lambda>cte. (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> ?P'72 a ct cta cnode cnodea slot slota cte s) and ?Q'63 a ct cta cnode cnodea slot slota cte\<rbrace>
 8. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a ct cta cnode\<rbrace> unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct))) \<lbrace>\<lambda>b. cte_wp_at (\<lambda>_. True) b and ?Q55 a ct cta cnode cnodea b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 a ct cta cnodea\<rbrace> unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta)) \<lbrace>\<lambda>b. pspace_aligned' and pspace_distinct' and ?Q'52 a ct cta cnode cnodea b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a ct\<rbrace> unify_failure (lookup_cap receiver (ct_receive_root ct)) \<lbrace>\<lambda>cnode. valid_objs and pspace_aligned and valid_cap cnode and ?Q35 a ct cta cnode\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> dc () ()
 2. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. True) \<oplus> (\<lambda>xs ys. ys = map cte_map xs)) (?R59 a ct cta cnode cnodea slot slota cap cte) (?R'59 a ct cta cnode cnodea slot slota cap cte) (returnOk [slot]) (returnOk [cte_map slot])
 3. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> \<lbrace>?Q61 a ct cta cnode cnodea slot slota cap\<rbrace> whenE (cap \<noteq> cap.NullCap) (throwError ()) \<lbrace>\<lambda>x. ?R59 a ct cta cnode cnodea slot slota cap cte\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'63 a ct cta cnode cnodea slot slota cte\<rbrace> whenE (cteCap cte \<noteq> capability.NullCap) (throwError ()) \<lbrace>\<lambda>x. ?R'59 a ct cta cnode cnodea slot slota cap cte\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q55 a ct cta cnode cnodea slot\<rbrace> get_cap slot \<lbrace>\<lambda>cap. (\<lambda>s. cap \<noteq> cap.NullCap \<longrightarrow> True) and ?Q61 a ct cta cnode cnodea slot slota cap\<rbrace>
 6. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 a ct cta cnode cnodea (cte_map slot)\<rbrace> getCTE (cte_map slot) \<lbrace>\<lambda>cte. (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> True) and ?Q'63 a ct cta cnode cnodea slot slota cte\<rbrace>
 7. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a ct cta cnode\<rbrace> unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct))) \<lbrace>\<lambda>b. cte_wp_at (\<lambda>_. True) b and ?Q55 a ct cta cnode cnodea b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 a ct cta cnodea\<rbrace> unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta)) \<lbrace>\<lambda>b. pspace_aligned' and pspace_distinct' and ?Q'52 a ct cta cnode cnodea b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a ct\<rbrace> unify_failure (lookup_cap receiver (ct_receive_root ct)) \<lbrace>\<lambda>cnode. valid_objs and pspace_aligned and valid_cap cnode and ?Q35 a ct cta cnode\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 a cta\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot cta)) \<lbrace>\<lambda>cnodea. valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' cnodea and ?Q'37 a ct cta cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> corres ((\<lambda>x y. True) \<oplus> (\<lambda>xs ys. ys = map cte_map xs)) (?R59 a ct cta cnode cnodea slot slota cap cte) (?R'59 a ct cta cnode cnodea slot slota cap cte) (returnOk [slot]) (returnOk [cte_map slot])
 2. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> \<lbrace>?Q61 a ct cta cnode cnodea slot slota cap\<rbrace> whenE (cap \<noteq> cap.NullCap) (throwError ()) \<lbrace>\<lambda>x. ?R59 a ct cta cnode cnodea slot slota cap cte\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'63 a ct cta cnode cnodea slot slota cte\<rbrace> whenE (cteCap cte \<noteq> capability.NullCap) (throwError ()) \<lbrace>\<lambda>x. ?R'59 a ct cta cnode cnodea slot slota cap cte\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q55 a ct cta cnode cnodea slot\<rbrace> get_cap slot \<lbrace>\<lambda>cap. (\<lambda>s. cap \<noteq> cap.NullCap \<longrightarrow> True) and ?Q61 a ct cta cnode cnodea slot slota cap\<rbrace>
 5. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 a ct cta cnode cnodea (cte_map slot)\<rbrace> getCTE (cte_map slot) \<lbrace>\<lambda>cte. (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> True) and ?Q'63 a ct cta cnode cnodea slot slota cte\<rbrace>
 6. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a ct cta cnode\<rbrace> unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct))) \<lbrace>\<lambda>b. cte_wp_at (\<lambda>_. True) b and ?Q55 a ct cta cnode cnodea b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 a ct cta cnodea\<rbrace> unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta)) \<lbrace>\<lambda>b. pspace_aligned' and pspace_distinct' and ?Q'52 a ct cta cnode cnodea b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a ct\<rbrace> unify_failure (lookup_cap receiver (ct_receive_root ct)) \<lbrace>\<lambda>cnode. valid_objs and pspace_aligned and valid_cap cnode and ?Q35 a ct cta cnode\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 a cta\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot cta)) \<lbrace>\<lambda>cnodea. valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' cnodea and ?Q'37 a ct cta cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q10 a\<rbrace> load_cap_transfer a \<lbrace>\<lambda>ct. valid_objs and pspace_aligned and tcb_at receiver and ?Q19 a ct\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> \<lbrace>?Q61 a ct cta cnode cnodea slot slota cap\<rbrace> whenE (cap \<noteq> cap.NullCap) (throwError ()) \<lbrace>\<lambda>x _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>a ct cta cnode cnodea slot slota cap cte. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot; cap_relation cap (cteCap cte)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'63 a ct cta cnode cnodea slot slota cte\<rbrace> whenE (cteCap cte \<noteq> capability.NullCap) (throwError ()) \<lbrace>\<lambda>x _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q55 a ct cta cnode cnodea slot\<rbrace> get_cap slot \<lbrace>\<lambda>cap. (\<lambda>s. cap \<noteq> cap.NullCap \<longrightarrow> True) and ?Q61 a ct cta cnode cnodea slot slota cap\<rbrace>
 4. \<And>a ct cta cnode cnodea slot slota. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea; slota = cte_map slot\<rbrakk> \<Longrightarrow> \<lbrace>?Q'52 a ct cta cnode cnodea (cte_map slot)\<rbrace> getCTE (cte_map slot) \<lbrace>\<lambda>cte. (\<lambda>s. cteCap cte \<noteq> capability.NullCap \<longrightarrow> True) and ?Q'63 a ct cta cnode cnodea slot slota cte\<rbrace>
 5. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 a ct cta cnode\<rbrace> unify_failure (lookup_slot_for_cnode_op False cnode (ct_receive_index ct) (unat (ct_receive_depth ct))) \<lbrace>\<lambda>b. cte_wp_at (\<lambda>_. True) b and ?Q55 a ct cta cnode cnodea b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a ct cta cnode cnodea. \<lbrakk>recv_buf = Some a; ct_relation ct cta; cap_relation cnode cnodea\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 a ct cta cnodea\<rbrace> unifyFailure (lookupSlotForCNodeOp False cnodea (ctReceiveIndex cta) (ctReceiveDepth cta)) \<lbrace>\<lambda>b. pspace_aligned' and pspace_distinct' and ?Q'52 a ct cta cnode cnodea b\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 a ct\<rbrace> unify_failure (lookup_cap receiver (ct_receive_root ct)) \<lbrace>\<lambda>cnode. valid_objs and pspace_aligned and valid_cap cnode and ?Q35 a ct cta cnode\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>a ct cta. \<lbrakk>recv_buf = Some a; ct_relation ct cta\<rbrakk> \<Longrightarrow> \<lbrace>?Q'21 a cta\<rbrace> unifyFailure (lookupCap receiver (ctReceiveRoot cta)) \<lbrace>\<lambda>cnodea. valid_objs' and pspace_aligned' and pspace_distinct' and valid_cap' cnodea and ?Q'37 a ct cta cnodea\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q10 a\<rbrace> load_cap_transfer a \<lbrace>\<lambda>ct. valid_objs and pspace_aligned and tcb_at receiver and ?Q19 a ct\<rbrace>
 10. \<And>a. recv_buf = Some a \<Longrightarrow> \<lbrace>?Q'10 a\<rbrace> loadCapTransfer a \<lbrace>\<lambda>cta. valid_objs' and pspace_distinct' and pspace_aligned' and tcb_at' receiver and ?Q'21 a cta\<rbrace>
A total of 12 subgoals... proof (prove)
goal:
No subgoals!