theory KHeap_DP

lemma decode_cnode_move_rvu:
  "\<lbrace>\<lambda>s. intent = CNodeMoveIntent dest_index dest_depth src_index src_depth \<and>
        get_index caps 0 = Some (cap ,cap_ref) \<and>
        src_cap \<noteq> NullCap \<and>
        (\<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow>
                    Q (MoveCall (src_cap')
                                (cap_object cap, offset src_index sz)
                                (cap_object target, offset dest_index sz')) s) \<and>
        unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and>
        unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth \<and>
        < \<box> (sz, (unat src_depth)):  cap src_index \<mapsto>u src_cap \<and>*
          \<box> (sz', (unat dest_depth)): target dest_index \<mapsto>u NullCap \<and>* R> s \<rbrace>
      decode_cnode_invocation target target_ref caps intent
     \<lbrace>\<lambda>rv s. Q rv s\<rbrace>, \<lbrace>Q'\<rbrace>" apply (unfold validE_def) apply (rule hoare_name_pre_state) apply (unfold validE_def[symmetric]) apply (clarsimp simp: decode_cnode_invocation_def split_def split: sum.splits) apply wp apply (simp add: if_apply_def2) apply (rule lookup_slot_for_cnode_op_rvu' [where r=sz and cap=src_cap and
       R="\<box> (sz', (unat dest_depth)): target dest_index \<mapsto>u NullCap \<and>* R"]) apply simp apply (rule ensure_empty_no_exception) apply (rule lookup_slot_for_cnode_op_rvu'[where r=sz' and cap=NullCap and
     R="\<box> (sz, (unat src_depth)): cap src_index \<mapsto>u src_cap \<and>* R"]) apply (simp, wp throw_on_none_rv validE_R_validE) apply (clarsimp split: option.splits) apply (intro conjI) apply (clarsimp simp:user_pointer_at_def Let_def) apply (clarsimp simp:sep_conj_assoc) apply (sep_solve) apply (clarsimp dest!: mapu_dest_opt_cap cap_type_null
                          reset_cap_asid_simps2[OF sym]
                    simp: cap_type_def) apply (sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. intent = CNodeMoveIntent dest_index dest_depth src_index src_depth \<and> get_index caps 0 = Some (cap, cap_ref) \<and> src_cap \<noteq> NullCap \<and> (\<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s) \<and> unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth \<and> cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrace> decode_cnode_invocation target target_ref caps intent \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. intent = CNodeMoveIntent dest_index dest_depth src_index src_depth \<and> get_index caps 0 = Some (cap, cap_ref) \<and> src_cap \<noteq> NullCap \<and> (\<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s) \<and> unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth \<and> cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrace> decode_cnode_invocation target target_ref caps intent \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> Q r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. intent = CNodeMoveIntent dest_index dest_depth src_index src_depth \<and> get_index caps 0 = Some (cap, cap_ref) \<and> src_cap \<noteq> NullCap \<and> (\<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s) \<and> unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth \<and> cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_cnode_invocation target target_ref caps intent \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> Q r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. intent = CNodeMoveIntent dest_index dest_depth src_index src_depth \<and> get_index caps 0 = Some (cap, cap_ref) \<and> src_cap \<noteq> NullCap \<and> (\<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s) \<and> unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> unat dest_depth \<le> word_bits \<and> 0 < unat dest_depth \<and> cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_cnode_invocation target target_ref caps intent \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<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);
y <- whenE (src_cap = NullCap) throw;
returnOk (MoveCall src_cap src_slot dest_slot)
odE \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s p dest_slot y. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> \<lbrace>?B14 s p dest_slot y\<rbrace> lookup_slot_for_cnode_op (fst p) src_index (unat src_depth) \<lbrace>\<lambda>src_slot s. opt_cap src_slot s \<noteq> None \<longrightarrow> (if the (opt_cap src_slot s) = NullCap then \<lambda>s. Q' undefined s \<and> True else Q (MoveCall (the (opt_cap src_slot s)) src_slot dest_slot)) s\<rbrace>, \<lbrace>Q'\<rbrace>
 2. \<And>s p dest_slot. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> \<lbrace>?B13 s p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>?B14 s p dest_slot\<rbrace>, \<lbrace>Q'\<rbrace>
 3. \<And>s p. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> \<lbrace>?B12 s p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B13 s p\<rbrace>, \<lbrace>Q'\<rbrace>
 4. \<And>s. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q11 s\<rbrace> throw_on_none (Some (cap, cap_ref)) \<lbrace>?B12 s\<rbrace>, \<lbrace>Q'\<rbrace>
 5. \<And>s sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; s = sa\<rbrakk> \<Longrightarrow> ?Q11 s sa proof (prove)
goal (5 subgoals):
 1. \<And>s p dest_slot. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> \<lbrace>?B14 s p dest_slot ()\<rbrace> lookup_slot_for_cnode_op (fst p) src_index (unat src_depth) \<lbrace>\<lambda>src_slot s. (\<exists>y. opt_cap src_slot s = Some y) \<longrightarrow> (the (opt_cap src_slot s) = NullCap \<longrightarrow> Q' undefined s) \<and> (the (opt_cap src_slot s) \<noteq> NullCap \<longrightarrow> Q (MoveCall (the (opt_cap src_slot s)) src_slot dest_slot) s)\<rbrace>, \<lbrace>Q'\<rbrace>
 2. \<And>s p dest_slot. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> \<lbrace>?B13 s p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>?B14 s p dest_slot\<rbrace>, \<lbrace>Q'\<rbrace>
 3. \<And>s p. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> \<lbrace>?B12 s p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B13 s p\<rbrace>, \<lbrace>Q'\<rbrace>
 4. \<And>s. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q11 s\<rbrace> throw_on_none (Some (cap, cap_ref)) \<lbrace>?B12 s\<rbrace>, \<lbrace>Q'\<rbrace>
 5. \<And>s sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; s = sa\<rbrakk> \<Longrightarrow> ?Q11 s sa proof (prove)
goal (4 subgoals):
 1. \<And>s p dest_slot. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> \<lbrace>?B13 s p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>\<lambda>a b. ((\<exists>y. opt_cap (cap_object (fst p), offset src_index sz) b = Some y) \<longrightarrow> (the (opt_cap (cap_object (fst p), offset src_index sz) b) = NullCap \<longrightarrow> Q' undefined b) \<and> (the (opt_cap (cap_object (fst p), offset src_index sz) b) \<noteq> NullCap \<longrightarrow> Q (MoveCall (the (opt_cap (cap_object (fst p), offset src_index sz) b)) (cap_object (fst p), offset src_index sz) dest_slot) b)) \<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>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) b\<rbrace>, \<lbrace>Q'\<rbrace>
 2. \<And>s p. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> \<lbrace>?B12 s p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B13 s p\<rbrace>, \<lbrace>Q'\<rbrace>
 3. \<And>s. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q11 s\<rbrace> throw_on_none (Some (cap, cap_ref)) \<lbrace>?B12 s\<rbrace>, \<lbrace>Q'\<rbrace>
 4. \<And>s sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; s = sa\<rbrakk> \<Longrightarrow> ?Q11 s sa proof (prove)
goal (4 subgoals):
 1. \<And>s p dest_slot. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> \<lbrace>?B13 s p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>\<lambda>a b. ((\<exists>y. opt_cap (cap_object (fst p), offset src_index sz) b = Some y) \<longrightarrow> (the (opt_cap (cap_object (fst p), offset src_index sz) b) = NullCap \<longrightarrow> Q' undefined b) \<and> (the (opt_cap (cap_object (fst p), offset src_index sz) b) \<noteq> NullCap \<longrightarrow> Q (MoveCall (the (opt_cap (cap_object (fst p), offset src_index sz) b)) (cap_object (fst p), offset src_index sz) dest_slot) b)) \<and> cdl.lift (\<box> (sz, unat src_depth) : fst p src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) b\<rbrace>, \<lbrace>Q'\<rbrace>
 2. \<And>s p. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> \<lbrace>?B12 s p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B13 s p\<rbrace>, \<lbrace>Q'\<rbrace>
 3. \<And>s. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q11 s\<rbrace> throw_on_none (Some (cap, cap_ref)) \<lbrace>?B12 s\<rbrace>, \<lbrace>Q'\<rbrace>
 4. \<And>s sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; s = sa\<rbrakk> \<Longrightarrow> ?Q11 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s p. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> \<lbrace>?B12 s p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>\<lambda>dest_slot. cdl.lift (dest_slot \<mapsto>c NullCap \<and>* ?R27 s p dest_slot) and (\<lambda>a. ((\<exists>y. opt_cap (cap_object (fst p), offset src_index sz) a = Some y) \<longrightarrow> (the (opt_cap (cap_object (fst p), offset src_index sz) a) = NullCap \<longrightarrow> Q' undefined a) \<and> (the (opt_cap (cap_object (fst p), offset src_index sz) a) \<noteq> NullCap \<longrightarrow> Q (MoveCall (the (opt_cap (cap_object (fst p), offset src_index sz) a)) (cap_object (fst p), offset src_index sz) dest_slot) a)) \<and> cdl.lift (\<box> (sz, unat src_depth) : fst p src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) a)\<rbrace>, \<lbrace>Q'\<rbrace>
 2. \<And>s. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q11 s\<rbrace> throw_on_none (Some (cap, cap_ref)) \<lbrace>?B12 s\<rbrace>, \<lbrace>Q'\<rbrace>
 3. \<And>s sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; s = sa\<rbrakk> \<Longrightarrow> ?Q11 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q11 s\<rbrace> throw_on_none (Some (cap, cap_ref)) \<lbrace>\<lambda>p sa. (cdl.lift ((cap_object target, offset dest_index sz') \<mapsto>c NullCap \<and>* ?R27 s p (cap_object target, offset dest_index sz')) and (\<lambda>a. ((\<exists>y. opt_cap (cap_object (fst p), offset src_index sz) a = Some y) \<longrightarrow> (the (opt_cap (cap_object (fst p), offset src_index sz) a) = NullCap \<longrightarrow> Q' undefined a) \<and> (the (opt_cap (cap_object (fst p), offset src_index sz) a) \<noteq> NullCap \<longrightarrow> Q (MoveCall (the (opt_cap (cap_object (fst p), offset src_index sz) a)) (cap_object (fst p), offset src_index sz) (cap_object target, offset dest_index sz')) a)) \<and> cdl.lift (\<box> (sz, unat src_depth) : fst p src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) a)) sa \<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>* \<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* R) sa\<rbrace>, \<lbrace>Q'\<rbrace>
 2. \<And>s sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; s = sa\<rbrakk> \<Longrightarrow> ?Q11 s sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) s; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; s = sa\<rbrakk> \<Longrightarrow> case Some (cap, cap_ref) of None \<Rightarrow> False | Some y \<Rightarrow> cdl.lift ((cap_object target, offset dest_index sz') \<mapsto>c NullCap \<and>* ?R27 s y (cap_object target, offset dest_index sz')) sa \<and> ((\<exists>ya. opt_cap (cap_object (fst y), offset src_index sz) sa = Some ya) \<longrightarrow> (the (opt_cap (cap_object (fst y), offset src_index sz) sa) = NullCap \<longrightarrow> Q' undefined sa) \<and> (the (opt_cap (cap_object (fst y), offset src_index sz) sa) \<noteq> NullCap \<longrightarrow> Q (MoveCall (the (opt_cap (cap_object (fst y), offset src_index sz) sa)) (cap_object (fst y), offset src_index sz) (cap_object target, offset dest_index sz')) sa)) \<and> cdl.lift (\<box> (sz, unat src_depth) : fst y src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa \<and> cdl.lift (\<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* \<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* R) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa\<rbrakk> \<Longrightarrow> cdl.lift ((cap_object target, offset dest_index sz') \<mapsto>c NullCap \<and>* ?R27 sa (cap, cap_ref) (cap_object target, offset dest_index sz')) sa \<and> ((\<exists>y. opt_cap (cap_object cap, offset src_index sz) sa = Some y) \<longrightarrow> (the (opt_cap (cap_object cap, offset src_index sz) sa) = NullCap \<longrightarrow> Q' undefined sa) \<and> (the (opt_cap (cap_object cap, offset src_index sz) sa) \<noteq> NullCap \<longrightarrow> Q (MoveCall (the (opt_cap (cap_object cap, offset src_index sz) sa)) (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) sa)) \<and> cdl.lift (\<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* \<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* R) sa proof (prove)
goal (3 subgoals):
 1. \<And>sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa\<rbrakk> \<Longrightarrow> cdl.lift ((cap_object target, offset dest_index sz') \<mapsto>c NullCap \<and>* ?R27 sa (cap, cap_ref) (cap_object target, offset dest_index sz')) sa
 2. \<And>sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa\<rbrakk> \<Longrightarrow> (\<exists>y. opt_cap (cap_object cap, offset src_index sz) sa = Some y) \<longrightarrow> (the (opt_cap (cap_object cap, offset src_index sz) sa) = NullCap \<longrightarrow> Q' undefined sa) \<and> (the (opt_cap (cap_object cap, offset src_index sz) sa) \<noteq> NullCap \<longrightarrow> Q (MoveCall (the (opt_cap (cap_object cap, offset src_index sz) sa)) (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) sa)
 3. \<And>sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* \<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* R) sa proof (prove)
goal (3 subgoals):
 1. \<And>sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; one_lvl_lookup target (unat dest_depth) sz'; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; 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 \<mapsto>f CNode (empty_cnode sz') \<and>* (cap_object target, offset dest_index sz') \<mapsto>c NullCap) \<and>* R) sa\<rbrakk> \<Longrightarrow> cdl.lift ((cap_object target, offset dest_index sz') \<mapsto>c NullCap \<and>* ?R27 sa (cap, cap_ref) (cap_object target, offset dest_index sz')) sa
 2. \<And>sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa\<rbrakk> \<Longrightarrow> (\<exists>y. opt_cap (cap_object cap, offset src_index sz) sa = Some y) \<longrightarrow> (the (opt_cap (cap_object cap, offset src_index sz) sa) = NullCap \<longrightarrow> Q' undefined sa) \<and> (the (opt_cap (cap_object cap, offset src_index sz) sa) \<noteq> NullCap \<longrightarrow> Q (MoveCall (the (opt_cap (cap_object cap, offset src_index sz) sa)) (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) sa)
 3. \<And>sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* \<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* R) sa proof (prove)
goal (3 subgoals):
 1. \<And>sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; one_lvl_lookup cap (unat src_depth) sz; guard_equal cap src_index (unat src_depth); is_cnode_cap cap; one_lvl_lookup target (unat dest_depth) sz'; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; 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 \<mapsto>f CNode (empty_cnode sz') \<and>* (cap_object target, offset dest_index sz') \<mapsto>c NullCap \<and>* R) sa\<rbrakk> \<Longrightarrow> cdl.lift ((cap_object target, offset dest_index sz') \<mapsto>c NullCap \<and>* ?R27 sa (cap, cap_ref) (cap_object target, offset dest_index sz')) sa
 2. \<And>sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa\<rbrakk> \<Longrightarrow> (\<exists>y. opt_cap (cap_object cap, offset src_index sz) sa = Some y) \<longrightarrow> (the (opt_cap (cap_object cap, offset src_index sz) sa) = NullCap \<longrightarrow> Q' undefined sa) \<and> (the (opt_cap (cap_object cap, offset src_index sz) sa) \<noteq> NullCap \<longrightarrow> Q (MoveCall (the (opt_cap (cap_object cap, offset src_index sz) sa)) (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) sa)
 3. \<And>sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* \<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* R) sa proof (prove)
goal (2 subgoals):
 1. \<And>sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa\<rbrakk> \<Longrightarrow> (\<exists>y. opt_cap (cap_object cap, offset src_index sz) sa = Some y) \<longrightarrow> (the (opt_cap (cap_object cap, offset src_index sz) sa) = NullCap \<longrightarrow> Q' undefined sa) \<and> (the (opt_cap (cap_object cap, offset src_index sz) sa) \<noteq> NullCap \<longrightarrow> Q (MoveCall (the (opt_cap (cap_object cap, offset src_index sz) sa)) (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) sa)
 2. \<And>sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* \<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* R) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>intent = CNodeMoveIntent dest_index dest_depth src_index src_depth; get_index caps 0 = Some (cap, cap_ref); src_cap \<noteq> NullCap; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall src_cap' (cap_object cap, offset src_index sz) (cap_object target, offset dest_index sz')) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; cdl.lift (\<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* \<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (sz', unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* \<box> (sz, unat src_depth) : cap src_index \<mapsto>u src_cap \<and>* R) sa proof (prove)
goal:
No subgoals!