theory CNode_DP

lemma decode_cnode_copy_same_parent_rvu:
  "\<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights;
   cap_object cap = cap_object target;
   get_index caps 0 = Some (cap ,cap_ref);
   \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap
     \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap'))
    (cap_object cap, offset src_index sz)
    (cap_object target, offset dest_index sz)) \<rbrakk> \<Longrightarrow>
  \<lbrace> K (one_lvl_lookup target (unat dest_depth) sz \<and>
  guard_equal target dest_index (unat dest_depth) \<and>
  is_cnode_cap target \<and>
  one_lvl_lookup cap (unat src_depth) sz \<and>
  guard_equal cap src_index (unat src_depth) \<and>
  is_cnode_cap cap) and
  < (cap_object cap) \<mapsto>f CNode (empty_cnode sz)
   \<and>* (cap_object cap, offset src_index sz) \<mapsto>c src_cap
   \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R>
  and K (unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and>
  unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth) \<rbrace>
  decode_cnode_invocation target target_ref caps intent
  \<lbrace>\<lambda>rv s. Q rv\<rbrace>, -" apply (clarsimp simp:user_pointer_at_def Let_def) apply (clarsimp simp: decode_cnode_invocation_def split_def split: sum.splits) apply (wp whenE_wp | simp)+ apply (rule validE_validE_R) apply (wp derive_cap_invE)+ apply (rule validE_validE_R) apply (rule lookup_slot_for_cnode_op_rvu' [where r=sz and cap=src_cap]) apply simp apply wp+ apply (rule validE_validE_R) apply (rule lookup_slot_for_cnode_op_rvu'[where r=sz and cap=NullCap]) apply (simp, wp throw_on_none_rv validE_R_validE) apply (clarsimp split: option.splits) apply (intro conjI) apply (clarsimp dest!: mapu_dest_opt_cap simp:conj_comms) apply (clarsimp simp: sep_conj_assoc user_pointer_at_def Let_def) apply sep_solve apply clarsimp apply (rule conjI) apply (sep_select_asm 2) apply (clarsimp dest!: opt_cap_sep_imp simp:conj_comms) apply (clarsimp simp: sep_conj_assoc user_pointer_at_def Let_def)+ apply sep_solve done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>K (one_lvl_lookup target (unat dest_depth) sz \<and> guard_equal target dest_index (unat dest_depth) \<and> is_cnode_cap target \<and> one_lvl_lookup cap (unat src_depth) sz \<and> guard_equal cap src_index (unat src_depth) \<and> is_cnode_cap cap) and cdl.lift (cap_object cap \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object cap, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) and K (unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth)\<rbrace> decode_cnode_invocation target target_ref caps intent \<lbrace>\<lambda>rv s. Q rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>y. one_lvl_lookup target (unat dest_depth) sz \<and> guard_equal target dest_index (unat dest_depth) \<and> is_cnode_cap target \<and> one_lvl_lookup cap (unat src_depth) sz \<and> guard_equal cap src_index (unat src_depth) \<and> is_cnode_cap cap) and cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) and (\<lambda>y. unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth)\<rbrace> decode_cnode_invocation target target_ref caps (CNodeCopyIntent dest_index dest_depth src_index src_depth rights) \<lbrace>\<lambda>rv s. Q rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>y. one_lvl_lookup target (unat dest_depth) sz \<and> guard_equal target dest_index (unat dest_depth) \<and> is_cnode_cap target \<and> one_lvl_lookup cap (unat src_depth) sz \<and> guard_equal cap src_index (unat src_depth) \<and> is_cnode_cap cap) and cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) and (\<lambda>y. unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth)\<rbrace> doE p <- throw_on_none (Some (cap, cap_ref));
dest_slot <- lookup_slot_for_cnode_op target dest_index (unat dest_depth);
y <- ensure_empty dest_slot;
src_slot <- lookup_slot_for_cnode_op (fst p) src_index (unat src_depth);
src_cap <- liftE (get_cap src_slot);
cap <- derive_cap src_slot (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap);
y <- whenE (cap = NullCap) throw;
returnOk (InsertCall cap src_slot dest_slot)
odE \<lbrace>\<lambda>rv s. Q rv\<rbrace>, - proof (prove)
goal (7 subgoals):
 1. \<And>p dest_slot src_slot src_capa. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?P'18 p dest_slot () src_slot src_capa\<rbrace> derive_cap src_slot (update_cap_rights (cap_rights src_capa \<inter> rights) src_capa) \<lbrace>\<lambda>cap. if cap = NullCap then \<lambda>s. True \<and> True else (\<lambda>a. Q (InsertCall cap src_slot dest_slot))\<rbrace>, -
 2. \<And>p dest_slot y src_slot. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?B7 p dest_slot y src_slot\<rbrace> liftE (get_cap src_slot) \<lbrace>\<lambda>src_cap s. True \<and> ?P'18 p dest_slot y src_slot src_cap s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>p dest_slot y. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?B6 p dest_slot y\<rbrace> lookup_slot_for_cnode_op (fst p) src_index (unat src_depth) \<lbrace>?B7 p dest_slot y\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>p dest_slot. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?B5 p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>?B6 p dest_slot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>p. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?B4 p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B5 p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?P'3\<rbrace> throw_on_none (Some (cap, cap_ref)) \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); ((\<lambda>y. one_lvl_lookup target (unat dest_depth) sz \<and> guard_equal target dest_index (unat dest_depth) \<and> is_cnode_cap target \<and> one_lvl_lookup cap (unat src_depth) sz \<and> guard_equal cap src_index (unat src_depth) \<and> is_cnode_cap cap) and cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) and (\<lambda>y. unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth)) s\<rbrakk> \<Longrightarrow> ?P'3 s proof (prove)
goal (7 subgoals):
 1. \<And>p dest_slot src_slot src_capa. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?P'18 p dest_slot () src_slot src_capa\<rbrace> derive_cap src_slot (update_cap_rights (cap_rights src_capa \<inter> rights) src_capa) \<lbrace>\<lambda>cap. if cap = NullCap then \<lambda>s. True \<and> True else (\<lambda>a. Q (InsertCall cap src_slot dest_slot))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>p dest_slot y src_slot. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?B7 p dest_slot y src_slot\<rbrace> liftE (get_cap src_slot) \<lbrace>\<lambda>src_cap s. True \<and> ?P'18 p dest_slot y src_slot src_cap s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>p dest_slot y. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?B6 p dest_slot y\<rbrace> lookup_slot_for_cnode_op (fst p) src_index (unat src_depth) \<lbrace>?B7 p dest_slot y\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>p dest_slot. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?B5 p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>?B6 p dest_slot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>p. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?B4 p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B5 p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?P'3\<rbrace> throw_on_none (Some (cap, cap_ref)) \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); ((\<lambda>y. one_lvl_lookup target (unat dest_depth) sz \<and> guard_equal target dest_index (unat dest_depth) \<and> is_cnode_cap target \<and> one_lvl_lookup cap (unat src_depth) sz \<and> guard_equal cap src_index (unat src_depth) \<and> is_cnode_cap cap) and cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) and (\<lambda>y. unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth)) s\<rbrakk> \<Longrightarrow> ?P'3 s proof (prove)
goal (5 subgoals):
 1. \<And>p dest_slot y. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?P'35 p dest_slot y\<rbrace> lookup_slot_for_cnode_op (fst p) src_index (unat src_depth) \<lbrace>\<lambda>rv s. opt_cap rv s \<noteq> None \<longrightarrow> True \<and> ((if derived_cap (update_cap_rights (cap_rights (the (opt_cap rv s)) \<inter> rights) (the (opt_cap rv s))) = NullCap then \<lambda>s. True \<and> True else (\<lambda>a. Q (InsertCall (derived_cap (update_cap_rights (cap_rights (the (opt_cap rv s)) \<inter> rights) (the (opt_cap rv s)))) rv dest_slot))) and (\<lambda>a. True)) s\<rbrace>, -
 2. \<And>p dest_slot. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?B5 p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>\<lambda>y s. True \<and> True \<and> ?P'35 p dest_slot y s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>p. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?B4 p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B5 p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?P'3\<rbrace> throw_on_none (Some (cap, cap_ref)) \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); ((\<lambda>y. one_lvl_lookup target (unat dest_depth) sz \<and> guard_equal target dest_index (unat dest_depth) \<and> is_cnode_cap target \<and> one_lvl_lookup cap (unat src_depth) sz \<and> guard_equal cap src_index (unat src_depth) \<and> is_cnode_cap cap) and cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) and (\<lambda>y. unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth)) s\<rbrakk> \<Longrightarrow> ?P'3 s proof (prove)
goal (5 subgoals):
 1. \<And>p dest_slot y. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?P'35 p dest_slot y\<rbrace> lookup_slot_for_cnode_op (fst p) src_index (unat src_depth) \<lbrace>\<lambda>rv s. opt_cap rv s \<noteq> None \<longrightarrow> True \<and> ((if derived_cap (update_cap_rights (cap_rights (the (opt_cap rv s)) \<inter> rights) (the (opt_cap rv s))) = NullCap then \<lambda>s. True \<and> True else (\<lambda>a. Q (InsertCall (derived_cap (update_cap_rights (cap_rights (the (opt_cap rv s)) \<inter> rights) (the (opt_cap rv s)))) rv dest_slot))) and (\<lambda>a. True)) s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>p dest_slot. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?B5 p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>\<lambda>y s. True \<and> True \<and> ?P'35 p dest_slot y s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>p. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?B4 p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B5 p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?P'3\<rbrace> throw_on_none (Some (cap, cap_ref)) \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); ((\<lambda>y. one_lvl_lookup target (unat dest_depth) sz \<and> guard_equal target dest_index (unat dest_depth) \<and> is_cnode_cap target \<and> one_lvl_lookup cap (unat src_depth) sz \<and> guard_equal cap src_index (unat src_depth) \<and> is_cnode_cap cap) and cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) and (\<lambda>y. unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth)) s\<rbrakk> \<Longrightarrow> ?P'3 s proof (prove)
goal (4 subgoals):
 1. \<And>p dest_slot. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?B5 p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>\<lambda>y s. True \<and> True \<and> (opt_cap (cap_object (fst p), offset src_index sz) s \<noteq> None \<longrightarrow> True \<and> ((if derived_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object (fst p), offset src_index sz) s)) \<inter> rights) (the (opt_cap (cap_object (fst p), offset src_index sz) s))) = NullCap then \<lambda>s. True \<and> True else (\<lambda>a. Q (InsertCall (derived_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object (fst p), offset src_index sz) s)) \<inter> rights) (the (opt_cap (cap_object (fst p), offset src_index sz) s)))) (cap_object (fst p), offset src_index sz) dest_slot))) and (\<lambda>a. True)) s) \<and> unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> cdl.lift (\<box> (sz, unat src_depth) : fst p src_index \<mapsto>u src_cap \<and>* ?R40 p dest_slot y) s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>p. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?B4 p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B5 p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?P'3\<rbrace> throw_on_none (Some (cap, cap_ref)) \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); ((\<lambda>y. one_lvl_lookup target (unat dest_depth) sz \<and> guard_equal target dest_index (unat dest_depth) \<and> is_cnode_cap target \<and> one_lvl_lookup cap (unat src_depth) sz \<and> guard_equal cap src_index (unat src_depth) \<and> is_cnode_cap cap) and cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) and (\<lambda>y. unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth)) s\<rbrakk> \<Longrightarrow> ?P'3 s proof (prove)
goal (4 subgoals):
 1. \<And>p dest_slot. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?B5 p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>\<lambda>y s. (derived_cap (the (opt_cap (cap_object (fst p), offset src_index sz) s)) = NullCap \<longrightarrow> unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> cdl.lift (\<box> (sz, unat src_depth) : fst p src_index \<mapsto>u src_cap \<and>* ?R40 p dest_slot ()) s) \<and> (derived_cap (the (opt_cap (cap_object (fst p), offset src_index sz) s)) \<noteq> NullCap \<longrightarrow> ((\<exists>y. opt_cap (cap_object (fst p), offset src_index sz) s = Some y) \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object (fst p), offset src_index sz) s)) \<inter> rights) (the (opt_cap (cap_object (fst p), offset src_index sz) s)))) (cap_object (fst p), offset src_index sz) dest_slot)) \<and> unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> cdl.lift (\<box> (sz, unat src_depth) : fst p src_index \<mapsto>u src_cap \<and>* ?R40 p dest_slot ()) s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>p. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?B4 p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B5 p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?P'3\<rbrace> throw_on_none (Some (cap, cap_ref)) \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); ((\<lambda>y. one_lvl_lookup target (unat dest_depth) sz \<and> guard_equal target dest_index (unat dest_depth) \<and> is_cnode_cap target \<and> one_lvl_lookup cap (unat src_depth) sz \<and> guard_equal cap src_index (unat src_depth) \<and> is_cnode_cap cap) and cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) and (\<lambda>y. unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth)) s\<rbrakk> \<Longrightarrow> ?P'3 s proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?P'76 p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>\<lambda>rv s. derived_cap (the (opt_cap (cap_object (fst p), offset src_index sz) s)) \<noteq> NullCap \<longrightarrow> ((\<exists>y. opt_cap (cap_object (fst p), offset src_index sz) s = Some y) \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object (fst p), offset src_index sz) s)) \<inter> rights) (the (opt_cap (cap_object (fst p), offset src_index sz) s)))) (cap_object (fst p), offset src_index sz) rv)) \<and> unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> cdl.lift (\<box> (sz, unat src_depth) : fst p src_index \<mapsto>u src_cap \<and>* ?R79 p ()) s\<rbrace>, -
 2. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?P'3\<rbrace> throw_on_none (Some (cap, cap_ref)) \<lbrace>\<lambda>p s. True \<and> True \<and> (derived_cap (the (opt_cap (cap_object (fst p), offset src_index sz) s)) = NullCap \<longrightarrow> unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> cdl.lift (\<box> (sz, unat src_depth) : fst p src_index \<mapsto>u src_cap \<and>* ?R79 p ()) s) \<and> ?P'76 p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); ((\<lambda>y. one_lvl_lookup target (unat dest_depth) sz \<and> guard_equal target dest_index (unat dest_depth) \<and> is_cnode_cap target \<and> one_lvl_lookup cap (unat src_depth) sz \<and> guard_equal cap src_index (unat src_depth) \<and> is_cnode_cap cap) and cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) and (\<lambda>y. unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth)) s\<rbrakk> \<Longrightarrow> ?P'3 s proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?P'76 p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>\<lambda>rv s. derived_cap (the (opt_cap (cap_object (fst p), offset src_index sz) s)) \<noteq> NullCap \<longrightarrow> ((\<exists>y. opt_cap (cap_object (fst p), offset src_index sz) s = Some y) \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object (fst p), offset src_index sz) s)) \<inter> rights) (the (opt_cap (cap_object (fst p), offset src_index sz) s)))) (cap_object (fst p), offset src_index sz) rv)) \<and> unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> cdl.lift (\<box> (sz, unat src_depth) : fst p src_index \<mapsto>u src_cap \<and>* ?R79 p ()) s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?P'3\<rbrace> throw_on_none (Some (cap, cap_ref)) \<lbrace>\<lambda>p s. True \<and> True \<and> (derived_cap (the (opt_cap (cap_object (fst p), offset src_index sz) s)) = NullCap \<longrightarrow> unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> cdl.lift (\<box> (sz, unat src_depth) : fst p src_index \<mapsto>u src_cap \<and>* ?R79 p ()) s) \<and> ?P'76 p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); ((\<lambda>y. one_lvl_lookup target (unat dest_depth) sz \<and> guard_equal target dest_index (unat dest_depth) \<and> is_cnode_cap target \<and> one_lvl_lookup cap (unat src_depth) sz \<and> guard_equal cap src_index (unat src_depth) \<and> is_cnode_cap cap) and cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) and (\<lambda>y. unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth)) s\<rbrakk> \<Longrightarrow> ?P'3 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))\<rbrakk> \<Longrightarrow> \<lbrace>?P'3\<rbrace> throw_on_none (Some (cap, cap_ref)) \<lbrace>\<lambda>p s. True \<and> True \<and> (derived_cap (the (opt_cap (cap_object (fst p), offset src_index sz) s)) = NullCap \<longrightarrow> unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> cdl.lift (\<box> (sz, unat src_depth) : fst p src_index \<mapsto>u src_cap \<and>* ?R79 p ()) s) \<and> (derived_cap (the (opt_cap (cap_object (fst p), offset src_index sz) s)) \<noteq> NullCap \<longrightarrow> ((\<exists>y. opt_cap (cap_object (fst p), offset src_index sz) s = Some y) \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object (fst p), offset src_index sz) s)) \<inter> rights) (the (opt_cap (cap_object (fst p), offset src_index sz) s)))) (cap_object (fst p), offset src_index sz) (cap_object target, offset dest_index sz))) \<and> unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> cdl.lift (\<box> (sz, unat src_depth) : fst p src_index \<mapsto>u src_cap \<and>* ?R79 p ()) s) \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth \<and> cdl.lift (\<box> (sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* ?R86 p) s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); ((\<lambda>y. one_lvl_lookup target (unat dest_depth) sz \<and> guard_equal target dest_index (unat dest_depth) \<and> is_cnode_cap target \<and> one_lvl_lookup cap (unat src_depth) sz \<and> guard_equal cap src_index (unat src_depth) \<and> is_cnode_cap cap) and cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) and (\<lambda>y. unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth)) s\<rbrakk> \<Longrightarrow> ?P'3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); ((\<lambda>y. one_lvl_lookup target (unat dest_depth) sz \<and> guard_equal target dest_index (unat dest_depth) \<and> is_cnode_cap target \<and> one_lvl_lookup cap (unat src_depth) sz \<and> guard_equal cap src_index (unat src_depth) \<and> is_cnode_cap cap) and cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) and (\<lambda>y. unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth)) s\<rbrakk> \<Longrightarrow> case Some (cap, cap_ref) of None \<Rightarrow> False | Some y \<Rightarrow> (derived_cap (the (opt_cap (cap_object (fst y), offset src_index sz) s)) = NullCap \<longrightarrow> unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> cdl.lift (\<box> (sz, unat src_depth) : fst y src_index \<mapsto>u src_cap \<and>* ?R79 y ()) s) \<and> (derived_cap (the (opt_cap (cap_object (fst y), offset src_index sz) s)) \<noteq> NullCap \<longrightarrow> ((\<exists>ya. opt_cap (cap_object (fst y), offset src_index sz) s = Some ya) \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object (fst y), offset src_index sz) s)) \<inter> rights) (the (opt_cap (cap_object (fst y), offset src_index sz) s)))) (cap_object (fst y), offset src_index sz) (cap_object target, offset dest_index sz))) \<and> unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> cdl.lift (\<box> (sz, unat src_depth) : fst y src_index \<mapsto>u src_cap \<and>* ?R79 y ()) s) \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth \<and> cdl.lift (\<box> (sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* ?R86 y) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth\<rbrakk> \<Longrightarrow> (derived_cap (the (opt_cap (cap_object target, offset src_index sz) s)) = NullCap \<longrightarrow> cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* ?R79 (cap, cap_ref) ()) s) \<and> (derived_cap (the (opt_cap (cap_object target, offset src_index sz) s)) \<noteq> NullCap \<longrightarrow> ((\<exists>y. opt_cap (cap_object target, offset src_index sz) s = Some y) \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object target, offset src_index sz) s)) \<inter> rights) (the (opt_cap (cap_object target, offset src_index sz) s)))) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))) \<and> cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* ?R79 (cap, cap_ref) ()) s) \<and> cdl.lift (\<box> (sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* ?R86 (cap, cap_ref)) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth\<rbrakk> \<Longrightarrow> derived_cap (the (opt_cap (cap_object target, offset src_index sz) s)) = NullCap \<longrightarrow> cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* ?R79 (cap, cap_ref) ()) s
 2. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth\<rbrakk> \<Longrightarrow> derived_cap (the (opt_cap (cap_object target, offset src_index sz) s)) \<noteq> NullCap \<longrightarrow> ((\<exists>y. opt_cap (cap_object target, offset src_index sz) s = Some y) \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object target, offset src_index sz) s)) \<inter> rights) (the (opt_cap (cap_object target, offset src_index sz) s)))) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))) \<and> cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* ?R79 (cap, cap_ref) ()) s
 3. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* ?R86 (cap, cap_ref)) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; derived_cap (the (opt_cap (cap_object target, offset src_index sz) s)) = NullCap\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* ?R79 (cap, cap_ref) ()) s
 2. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth\<rbrakk> \<Longrightarrow> derived_cap (the (opt_cap (cap_object target, offset src_index sz) s)) \<noteq> NullCap \<longrightarrow> ((\<exists>y. opt_cap (cap_object target, offset src_index sz) s = Some y) \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object target, offset src_index sz) s)) \<inter> rights) (the (opt_cap (cap_object target, offset src_index sz) s)))) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))) \<and> cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* ?R79 (cap, cap_ref) ()) s
 3. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* ?R86 (cap, cap_ref)) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; derived_cap (the (opt_cap (cap_object target, offset src_index sz) s)) = NullCap\<rbrakk> \<Longrightarrow> cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* ?R79 (cap, cap_ref) ()) s
 2. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth\<rbrakk> \<Longrightarrow> derived_cap (the (opt_cap (cap_object target, offset src_index sz) s)) \<noteq> NullCap \<longrightarrow> ((\<exists>y. opt_cap (cap_object target, offset src_index sz) s = Some y) \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object target, offset src_index sz) s)) \<inter> rights) (the (opt_cap (cap_object target, offset src_index sz) s)))) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))) \<and> cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* ?R79 (cap, cap_ref) ()) s
 3. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* ?R86 (cap, cap_ref)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth\<rbrakk> \<Longrightarrow> derived_cap (the (opt_cap (cap_object target, offset src_index sz) s)) \<noteq> NullCap \<longrightarrow> ((\<exists>y. opt_cap (cap_object target, offset src_index sz) s = Some y) \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object target, offset src_index sz) s)) \<inter> rights) (the (opt_cap (cap_object target, offset src_index sz) s)))) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))) \<and> cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s
 2. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* ?R86 (cap, cap_ref)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; derived_cap (the (opt_cap (cap_object target, offset src_index sz) s)) \<noteq> NullCap\<rbrakk> \<Longrightarrow> ((\<exists>y. opt_cap (cap_object target, offset src_index sz) s = Some y) \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object target, offset src_index sz) s)) \<inter> rights) (the (opt_cap (cap_object target, offset src_index sz) s)))) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))) \<and> cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s
 2. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* ?R86 (cap, cap_ref)) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; derived_cap (the (opt_cap (cap_object target, offset src_index sz) s)) \<noteq> NullCap\<rbrakk> \<Longrightarrow> (\<exists>y. opt_cap (cap_object target, offset src_index sz) s = Some y) \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object target, offset src_index sz) s)) \<inter> rights) (the (opt_cap (cap_object target, offset src_index sz) s)))) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))
 2. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; derived_cap (the (opt_cap (cap_object target, offset src_index sz) s)) \<noteq> NullCap\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s
 3. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* ?R86 (cap, cap_ref)) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; derived_cap (the (opt_cap (cap_object target, offset src_index sz) s)) \<noteq> NullCap; cdl.lift ((cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> (\<exists>y. opt_cap (cap_object target, offset src_index sz) s = Some y) \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object target, offset src_index sz) s)) \<inter> rights) (the (opt_cap (cap_object target, offset src_index sz) s)))) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz))
 2. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; derived_cap (the (opt_cap (cap_object target, offset src_index sz) s)) \<noteq> NullCap\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s
 3. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* ?R86 (cap, cap_ref)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; derived_cap (the (opt_cap (cap_object target, offset src_index sz) s)) \<noteq> NullCap\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s
 2. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* ?R86 (cap, cap_ref)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>intent = CNodeCopyIntent dest_index dest_depth src_index src_depth rights; cap_object cap = cap_object target; get_index caps 0 = Some (cap, cap_ref); \<forall>cap'. reset_cap_asid cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_rights (cap_rights cap' \<inter> rights) cap')) (cap_object target, offset src_index sz) (cap_object target, offset dest_index sz)); one_lvl_lookup target (unat dest_depth) sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset src_index sz) \<mapsto>c src_cap \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* R) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth\<rbrakk> \<Longrightarrow> cdl.lift (cap_object target \<mapsto>f CNode (empty_cnode sz) \<and>* (cap_object target, offset dest_index sz) \<mapsto>c NullCap \<and>* ?R86 (cap, cap_ref)) s proof (prove)
goal:
No subgoals!