theory KHeap_DP

lemma decode_cnode_mutate_rvu:
  "\<lbrace>\<lambda>s. caps \<noteq> []
    \<and> < \<box> (src_sz, (unat src_depth)):  (fst (the $ get_index caps 0)) src_index \<mapsto>u src_cap
    \<and>* \<box> (dest_sz, (unat dest_depth)):  target dest_index \<mapsto>u NullCap \<and>* R> s
    \<and>  valid_src_cap src_cap badge \<and> \<not> ep_related_cap src_cap \<and> cap_has_type src_cap
    \<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> (\<forall>src_cap'. reset_cap_asid src_cap'
       = reset_cap_asid src_cap
       \<longrightarrow>  Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the $ get_index caps 0)), offset src_index src_sz)
            (cap_object target, offset dest_index dest_sz)) s)\<rbrace>
    decode_cnode_invocation target target_ref caps
     (CNodeMutateIntent dest_index dest_depth src_index src_depth badge)
   \<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 apply (frule cap_type_null) apply (clarsimp simp: decode_cnode_invocation_def split_def neq_Nil_conv
    split:sum.splits) apply wp apply (wp update_cap_data)+ apply (simp add: if_apply_def2) apply (rule lookup_slot_for_cnode_op_rvu' [where r=src_sz and cap=src_cap and
       R="\<box> (dest_sz, (unat dest_depth)): target dest_index \<mapsto>u NullCap \<and>* R"]) apply simp apply (rule ensure_empty_no_exception) apply (rule_tac R="\<box> (src_sz, (unat src_depth)): a src_index \<mapsto>u src_cap \<and>* R" in
     lookup_slot_for_cnode_op_rvu'[where r=dest_sz and cap=NullCap]) apply (simp, wp throw_on_none_rv validE_R_validE) apply (clarsimp simp:Let_def get_index_def 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
     simp: conj_comms update_cap_data_non cong:non_cap_cong) apply (subst (asm) reset_cap_asid_ep_related_cap[OF sym], assumption) apply (metis reset_cap_asid_cap_type valid_src_cap_asid_cong ep_related_capI(1-2)) apply sep_solve done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. caps \<noteq> [] \<and> cdl.lift (\<box> (src_sz, unat src_depth) : fst (the $ get_index caps 0) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s \<and> valid_src_cap src_cap badge \<and> \<not> ep_related_cap src_cap \<and> cap_has_type src_cap \<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> (\<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the $ get_index caps 0)), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s)\<rbrace> decode_cnode_invocation target target_ref caps (CNodeMutateIntent dest_index dest_depth src_index src_depth badge) \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. caps \<noteq> [] \<and> cdl.lift (\<box> (src_sz, unat src_depth) : fst (the $ get_index caps 0) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s \<and> valid_src_cap src_cap badge \<and> \<not> ep_related_cap src_cap \<and> cap_has_type src_cap \<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> (\<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the $ get_index caps 0)), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s)\<rbrace> decode_cnode_invocation target target_ref caps (CNodeMutateIntent dest_index dest_depth src_index src_depth badge) \<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. caps \<noteq> [] \<and> cdl.lift (\<box> (src_sz, unat src_depth) : fst (the $ get_index caps 0) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s \<and> valid_src_cap src_cap badge \<and> \<not> ep_related_cap src_cap \<and> cap_has_type src_cap \<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> (\<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the $ get_index caps 0)), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s) \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_cnode_invocation target target_ref caps (CNodeMutateIntent dest_index dest_depth src_index src_depth badge) \<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. caps \<noteq> [] \<and> cdl.lift (\<box> (src_sz, unat src_depth) : fst (the $ get_index caps 0) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s \<and> valid_src_cap src_cap badge \<and> \<not> ep_related_cap src_cap \<and> cap_has_type src_cap \<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> (\<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the $ get_index caps 0)), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s) \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_cnode_invocation target target_ref caps (CNodeMutateIntent dest_index dest_depth src_index src_depth badge) \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s type. \<lbrakk>caps \<noteq> []; cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index caps 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index caps 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_cnode_invocation target target_ref caps (CNodeMutateIntent dest_index dest_depth src_index src_depth badge) \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s type. \<lbrakk>caps \<noteq> []; cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index caps 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index caps 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_cnode_invocation target target_ref caps (CNodeMutateIntent dest_index dest_depth src_index src_depth badge) \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s type a aa b ys. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE p <- throw_on_none (get_index ((a, aa, b) # ys) 0);
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 <- liftE (update_cap_data True badge src_cap);
y <- whenE (cap = NullCap) throw;
returnOk (MoveCall cap src_slot dest_slot)
odE \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>s type a aa b ys p dest_slot y src_slot src_capa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?B26 s type a aa b ys p dest_slot y src_slot src_capa\<rbrace> update_cap_data True badge src_capa \<lbrace>\<lambda>cap. if cap = NullCap then \<lambda>s. Q' undefined s \<and> True else Q (MoveCall cap src_slot dest_slot)\<rbrace>
 2. \<And>s type a aa b ys p dest_slot y src_slot. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?B25 s type a aa b ys p dest_slot y src_slot\<rbrace> liftE (get_cap src_slot) \<lbrace>?B26 s type a aa b ys p dest_slot y src_slot\<rbrace>, \<lbrace>Q'\<rbrace>
 3. \<And>s type a aa b ys p dest_slot y. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?B24 s type a aa b ys p dest_slot y\<rbrace> lookup_slot_for_cnode_op (fst p) src_index (unat src_depth) \<lbrace>?B25 s type a aa b ys p dest_slot y\<rbrace>, \<lbrace>Q'\<rbrace>
 4. \<And>s type a aa b ys p dest_slot. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?B23 s type a aa b ys p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>?B24 s type a aa b ys p dest_slot\<rbrace>, \<lbrace>Q'\<rbrace>
 5. \<And>s type a aa b ys p. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s type a aa b ys p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B23 s type a aa b ys p\<rbrace>, \<lbrace>Q'\<rbrace>
 6. \<And>s type a aa b ys. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 s type a aa b ys\<rbrace> throw_on_none (get_index ((a, aa, b) # ys) 0) \<lbrace>?B22 s type a aa b ys\<rbrace>, \<lbrace>Q'\<rbrace>
 7. \<And>s type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys; s = sa\<rbrakk> \<Longrightarrow> ?Q21 s type a aa b ys sa proof (prove)
goal (5 subgoals):
 1. \<And>s type a aa b ys p dest_slot y. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?B24 s type a aa b ys 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> valid_src_cap (the (opt_cap src_slot s)) badge \<and> cap_has_type (the (opt_cap src_slot s)) \<and> (is_ep_cap (the (opt_cap src_slot s)) \<or> is_ntfn_cap (the (opt_cap src_slot s)) \<longrightarrow> \<not> True \<and> cap_badge (the (opt_cap src_slot s)) = 0) \<and> (if update_cap_data_det badge (the (opt_cap src_slot s)) = NullCap then \<lambda>s. Q' undefined s \<and> True else Q (MoveCall (update_cap_data_det badge (the (opt_cap src_slot s))) src_slot dest_slot)) s\<rbrace>, \<lbrace>Q'\<rbrace>
 2. \<And>s type a aa b ys p dest_slot. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?B23 s type a aa b ys p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>?B24 s type a aa b ys p dest_slot\<rbrace>, \<lbrace>Q'\<rbrace>
 3. \<And>s type a aa b ys p. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s type a aa b ys p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B23 s type a aa b ys p\<rbrace>, \<lbrace>Q'\<rbrace>
 4. \<And>s type a aa b ys. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 s type a aa b ys\<rbrace> throw_on_none (get_index ((a, aa, b) # ys) 0) \<lbrace>?B22 s type a aa b ys\<rbrace>, \<lbrace>Q'\<rbrace>
 5. \<And>s type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys; s = sa\<rbrakk> \<Longrightarrow> ?Q21 s type a aa b ys sa proof (prove)
goal (5 subgoals):
 1. \<And>s type a aa b ys p dest_slot. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?B24 s type a aa b ys 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> valid_src_cap (the (opt_cap src_slot s)) badge \<and> cap_has_type (the (opt_cap src_slot s)) \<and> cap_type (the (opt_cap src_slot s)) \<noteq> Some EndpointType \<and> cap_type (the (opt_cap src_slot s)) \<noteq> Some NotificationType \<and> (update_cap_data_det badge (the (opt_cap src_slot s)) = NullCap \<longrightarrow> Q' undefined s) \<and> (update_cap_data_det badge (the (opt_cap src_slot s)) \<noteq> NullCap \<longrightarrow> Q (MoveCall (update_cap_data_det badge (the (opt_cap src_slot s))) src_slot dest_slot) s)\<rbrace>, \<lbrace>Q'\<rbrace>
 2. \<And>s type a aa b ys p dest_slot. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?B23 s type a aa b ys p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>?B24 s type a aa b ys p dest_slot\<rbrace>, \<lbrace>Q'\<rbrace>
 3. \<And>s type a aa b ys p. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s type a aa b ys p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B23 s type a aa b ys p\<rbrace>, \<lbrace>Q'\<rbrace>
 4. \<And>s type a aa b ys. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 s type a aa b ys\<rbrace> throw_on_none (get_index ((a, aa, b) # ys) 0) \<lbrace>?B22 s type a aa b ys\<rbrace>, \<lbrace>Q'\<rbrace>
 5. \<And>s type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys; s = sa\<rbrakk> \<Longrightarrow> ?Q21 s type a aa b ys sa proof (prove)
goal (4 subgoals):
 1. \<And>s type a aa b ys p dest_slot. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?B23 s type a aa b ys p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>\<lambda>a b. ((\<exists>y. opt_cap (cap_object (fst p), offset src_index src_sz) b = Some y) \<longrightarrow> valid_src_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) b)) badge \<and> cap_has_type (the (opt_cap (cap_object (fst p), offset src_index src_sz) b)) \<and> cap_type (the (opt_cap (cap_object (fst p), offset src_index src_sz) b)) \<noteq> Some EndpointType \<and> cap_type (the (opt_cap (cap_object (fst p), offset src_index src_sz) b)) \<noteq> Some NotificationType \<and> (update_cap_data_det badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) b)) = NullCap \<longrightarrow> Q' undefined b) \<and> (update_cap_data_det badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) b)) \<noteq> NullCap \<longrightarrow> Q (MoveCall (update_cap_data_det badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) b))) (cap_object (fst p), offset src_index src_sz) dest_slot) b)) \<and> unat src_depth \<le> word_bits \<and> 0 < unat src_depth \<and> cdl.lift (\<box> (src_sz, unat src_depth) : fst p src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) b\<rbrace>, \<lbrace>Q'\<rbrace>
 2. \<And>s type a aa b ys p. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s type a aa b ys p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B23 s type a aa b ys p\<rbrace>, \<lbrace>Q'\<rbrace>
 3. \<And>s type a aa b ys. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 s type a aa b ys\<rbrace> throw_on_none (get_index ((a, aa, b) # ys) 0) \<lbrace>?B22 s type a aa b ys\<rbrace>, \<lbrace>Q'\<rbrace>
 4. \<And>s type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys; s = sa\<rbrakk> \<Longrightarrow> ?Q21 s type a aa b ys sa proof (prove)
goal (4 subgoals):
 1. \<And>s type a aa b ys p dest_slot. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?B23 s type a aa b ys p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>\<lambda>a b. ((\<exists>y. opt_cap (cap_object (fst p), offset src_index src_sz) b = Some y) \<longrightarrow> valid_src_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) b)) badge \<and> cap_has_type (the (opt_cap (cap_object (fst p), offset src_index src_sz) b)) \<and> cap_type (the (opt_cap (cap_object (fst p), offset src_index src_sz) b)) \<noteq> Some EndpointType \<and> cap_type (the (opt_cap (cap_object (fst p), offset src_index src_sz) b)) \<noteq> Some NotificationType \<and> (update_cap_data_det badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) b)) = NullCap \<longrightarrow> Q' undefined b) \<and> (update_cap_data_det badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) b)) \<noteq> NullCap \<longrightarrow> Q (MoveCall (update_cap_data_det badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) b))) (cap_object (fst p), offset src_index src_sz) dest_slot) b)) \<and> cdl.lift (\<box> (src_sz, unat src_depth) : fst p src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) b\<rbrace>, \<lbrace>Q'\<rbrace>
 2. \<And>s type a aa b ys p. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s type a aa b ys p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B23 s type a aa b ys p\<rbrace>, \<lbrace>Q'\<rbrace>
 3. \<And>s type a aa b ys. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 s type a aa b ys\<rbrace> throw_on_none (get_index ((a, aa, b) # ys) 0) \<lbrace>?B22 s type a aa b ys\<rbrace>, \<lbrace>Q'\<rbrace>
 4. \<And>s type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys; s = sa\<rbrakk> \<Longrightarrow> ?Q21 s type a aa b ys sa proof (prove)
goal (3 subgoals):
 1. \<And>s type a aa b ys p. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s type a aa b ys 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>* ?R44 s type a aa b ys p dest_slot) and (\<lambda>a. ((\<exists>y. opt_cap (cap_object (fst p), offset src_index src_sz) a = Some y) \<longrightarrow> valid_src_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) a)) badge \<and> cap_has_type (the (opt_cap (cap_object (fst p), offset src_index src_sz) a)) \<and> cap_type (the (opt_cap (cap_object (fst p), offset src_index src_sz) a)) \<noteq> Some EndpointType \<and> cap_type (the (opt_cap (cap_object (fst p), offset src_index src_sz) a)) \<noteq> Some NotificationType \<and> (update_cap_data_det badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) a)) = NullCap \<longrightarrow> Q' undefined a) \<and> (update_cap_data_det badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) a)) \<noteq> NullCap \<longrightarrow> Q (MoveCall (update_cap_data_det badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) a))) (cap_object (fst p), offset src_index src_sz) dest_slot) a)) \<and> cdl.lift (\<box> (src_sz, unat src_depth) : fst p src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) a)\<rbrace>, \<lbrace>Q'\<rbrace>
 2. \<And>s type a aa b ys. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 s type a aa b ys\<rbrace> throw_on_none (get_index ((a, aa, b) # ys) 0) \<lbrace>?B22 s type a aa b ys\<rbrace>, \<lbrace>Q'\<rbrace>
 3. \<And>s type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys; s = sa\<rbrakk> \<Longrightarrow> ?Q21 s type a aa b ys sa proof (prove)
goal (2 subgoals):
 1. \<And>s type a aa b ys. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 s type a aa b ys\<rbrace> throw_on_none (get_index ((a, aa, b) # ys) 0) \<lbrace>\<lambda>p sa. (cdl.lift ((cap_object target, offset dest_index dest_sz) \<mapsto>c NullCap \<and>* ?R44 s type a aa b ys p (cap_object target, offset dest_index dest_sz)) and (\<lambda>a. ((\<exists>y. opt_cap (cap_object (fst p), offset src_index src_sz) a = Some y) \<longrightarrow> valid_src_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) a)) badge \<and> cap_has_type (the (opt_cap (cap_object (fst p), offset src_index src_sz) a)) \<and> cap_type (the (opt_cap (cap_object (fst p), offset src_index src_sz) a)) \<noteq> Some EndpointType \<and> cap_type (the (opt_cap (cap_object (fst p), offset src_index src_sz) a)) \<noteq> Some NotificationType \<and> (update_cap_data_det badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) a)) = NullCap \<longrightarrow> Q' undefined a) \<and> (update_cap_data_det badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) a)) \<noteq> NullCap \<longrightarrow> Q (MoveCall (update_cap_data_det badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) a))) (cap_object (fst p), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) a)) \<and> cdl.lift (\<box> (src_sz, unat src_depth) : fst p src_index \<mapsto>u src_cap \<and>* \<box> (dest_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> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* \<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* R) sa\<rbrace>, \<lbrace>Q'\<rbrace>
 2. \<And>s type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys; s = sa\<rbrakk> \<Longrightarrow> ?Q21 s type a aa b ys sa proof (prove)
goal (1 subgoal):
 1. \<And>s type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : fst (the (get_index ((a, aa, b) # ys) 0)) src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) s; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object (fst (the (get_index ((a, aa, b) # ys) 0))), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys; s = sa\<rbrakk> \<Longrightarrow> case get_index ((a, aa, b) # ys) 0 of None \<Rightarrow> False | Some y \<Rightarrow> cdl.lift ((cap_object target, offset dest_index dest_sz) \<mapsto>c NullCap \<and>* ?R44 s type a aa b ys y (cap_object target, offset dest_index dest_sz)) sa \<and> ((\<exists>ya. opt_cap (cap_object (fst y), offset src_index src_sz) sa = Some ya) \<longrightarrow> valid_src_cap (the (opt_cap (cap_object (fst y), offset src_index src_sz) sa)) badge \<and> cap_has_type (the (opt_cap (cap_object (fst y), offset src_index src_sz) sa)) \<and> cap_type (the (opt_cap (cap_object (fst y), offset src_index src_sz) sa)) \<noteq> Some EndpointType \<and> cap_type (the (opt_cap (cap_object (fst y), offset src_index src_sz) sa)) \<noteq> Some NotificationType \<and> (update_cap_data_det badge (the (opt_cap (cap_object (fst y), offset src_index src_sz) sa)) = NullCap \<longrightarrow> Q' undefined sa) \<and> (update_cap_data_det badge (the (opt_cap (cap_object (fst y), offset src_index src_sz) sa)) \<noteq> NullCap \<longrightarrow> Q (MoveCall (update_cap_data_det badge (the (opt_cap (cap_object (fst y), offset src_index src_sz) sa))) (cap_object (fst y), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa)) \<and> cdl.lift (\<box> (src_sz, unat src_depth) : fst y src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa \<and> cdl.lift (\<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* \<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* R) sa proof (prove)
goal (1 subgoal):
 1. \<And>type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> cdl.lift ((cap_object target, offset dest_index dest_sz) \<mapsto>c NullCap \<and>* ?R44 sa type a aa b ys (a, aa, b) (cap_object target, offset dest_index dest_sz)) sa \<and> ((\<exists>y. opt_cap (cap_object a, offset src_index src_sz) sa = Some y) \<longrightarrow> valid_src_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) badge \<and> cap_has_type (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<and> cap_type (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> Some EndpointType \<and> cap_type (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> Some NotificationType \<and> (update_cap_data_det badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) = NullCap \<longrightarrow> Q' undefined sa) \<and> (update_cap_data_det badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> NullCap \<longrightarrow> Q (MoveCall (update_cap_data_det badge (the (opt_cap (cap_object a, offset src_index src_sz) sa))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa)) \<and> cdl.lift (\<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* \<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* R) sa proof (prove)
goal (3 subgoals):
 1. \<And>type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> cdl.lift ((cap_object target, offset dest_index dest_sz) \<mapsto>c NullCap \<and>* ?R44 sa type a aa b ys (a, aa, b) (cap_object target, offset dest_index dest_sz)) sa
 2. \<And>type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> (\<exists>y. opt_cap (cap_object a, offset src_index src_sz) sa = Some y) \<longrightarrow> valid_src_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) badge \<and> cap_has_type (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<and> cap_type (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> Some EndpointType \<and> cap_type (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> Some NotificationType \<and> (update_cap_data_det badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) = NullCap \<longrightarrow> Q' undefined sa) \<and> (update_cap_data_det badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> NullCap \<longrightarrow> Q (MoveCall (update_cap_data_det badge (the (opt_cap (cap_object a, offset src_index src_sz) sa))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa)
 3. \<And>type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* \<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* R) sa proof (prove)
goal (3 subgoals):
 1. \<And>type a aa b ys sa. \<lbrakk>valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys; one_lvl_lookup a (unat src_depth) src_sz; guard_equal a src_index (unat src_depth); is_cnode_cap a; one_lvl_lookup target (unat dest_depth) dest_sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; cdl.lift ((cap_object a \<mapsto>f CNode (empty_cnode src_sz) \<and>* (cap_object a, offset src_index src_sz) \<mapsto>c src_cap) \<and>* (cap_object target \<mapsto>f CNode (empty_cnode dest_sz) \<and>* (cap_object target, offset dest_index dest_sz) \<mapsto>c NullCap) \<and>* R) sa\<rbrakk> \<Longrightarrow> cdl.lift ((cap_object target, offset dest_index dest_sz) \<mapsto>c NullCap \<and>* ?R44 sa type a aa b ys (a, aa, b) (cap_object target, offset dest_index dest_sz)) sa
 2. \<And>type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> (\<exists>y. opt_cap (cap_object a, offset src_index src_sz) sa = Some y) \<longrightarrow> valid_src_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) badge \<and> cap_has_type (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<and> cap_type (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> Some EndpointType \<and> cap_type (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> Some NotificationType \<and> (update_cap_data_det badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) = NullCap \<longrightarrow> Q' undefined sa) \<and> (update_cap_data_det badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> NullCap \<longrightarrow> Q (MoveCall (update_cap_data_det badge (the (opt_cap (cap_object a, offset src_index src_sz) sa))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa)
 3. \<And>type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* \<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* R) sa proof (prove)
goal (3 subgoals):
 1. \<And>type a aa b ys sa. \<lbrakk>valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys; one_lvl_lookup a (unat src_depth) src_sz; guard_equal a src_index (unat src_depth); is_cnode_cap a; one_lvl_lookup target (unat dest_depth) dest_sz; guard_equal target dest_index (unat dest_depth); is_cnode_cap target; cdl.lift (cap_object a \<mapsto>f CNode (empty_cnode src_sz) \<and>* (cap_object a, offset src_index src_sz) \<mapsto>c src_cap \<and>* cap_object target \<mapsto>f CNode (empty_cnode dest_sz) \<and>* (cap_object target, offset dest_index dest_sz) \<mapsto>c NullCap \<and>* R) sa\<rbrakk> \<Longrightarrow> cdl.lift ((cap_object target, offset dest_index dest_sz) \<mapsto>c NullCap \<and>* ?R44 sa type a aa b ys (a, aa, b) (cap_object target, offset dest_index dest_sz)) sa
 2. \<And>type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> (\<exists>y. opt_cap (cap_object a, offset src_index src_sz) sa = Some y) \<longrightarrow> valid_src_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) badge \<and> cap_has_type (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<and> cap_type (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> Some EndpointType \<and> cap_type (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> Some NotificationType \<and> (update_cap_data_det badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) = NullCap \<longrightarrow> Q' undefined sa) \<and> (update_cap_data_det badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> NullCap \<longrightarrow> Q (MoveCall (update_cap_data_det badge (the (opt_cap (cap_object a, offset src_index src_sz) sa))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa)
 3. \<And>type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* \<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* R) sa proof (prove)
goal (2 subgoals):
 1. \<And>type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> (\<exists>y. opt_cap (cap_object a, offset src_index src_sz) sa = Some y) \<longrightarrow> valid_src_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) badge \<and> cap_has_type (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<and> cap_type (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> Some EndpointType \<and> cap_type (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> Some NotificationType \<and> (update_cap_data_det badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) = NullCap \<longrightarrow> Q' undefined sa) \<and> (update_cap_data_det badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> NullCap \<longrightarrow> Q (MoveCall (update_cap_data_det badge (the (opt_cap (cap_object a, offset src_index src_sz) sa))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa)
 2. \<And>type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* \<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* R) sa proof (prove)
goal (2 subgoals):
 1. \<And>type a aa b ys sa cap'. \<lbrakk>valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'\<rbrakk> \<Longrightarrow> valid_src_cap cap' badge \<and> cap_type cap' \<noteq> Some EndpointType \<and> cap_type cap' \<noteq> Some NotificationType \<and> cap_has_type cap'
 2. \<And>type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* \<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* R) sa proof (prove)
goal (2 subgoals):
 1. \<And>type a aa b ys sa cap'. \<lbrakk>valid_src_cap src_cap badge; \<not> ep_related_cap cap'; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'\<rbrakk> \<Longrightarrow> valid_src_cap cap' badge \<and> cap_type cap' \<noteq> Some EndpointType \<and> cap_type cap' \<noteq> Some NotificationType \<and> cap_has_type cap'
 2. \<And>type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* \<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* R) sa proof (prove)
goal (1 subgoal):
 1. \<And>type a aa b ys sa. \<lbrakk>cdl.lift (\<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* \<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* R) sa; valid_src_cap src_cap badge; \<not> ep_related_cap src_cap; cap_type src_cap = Some type; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (MoveCall (update_cap_data_det badge src_cap') (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; src_cap \<noteq> NullCap; caps = (a, aa, b) # ys\<rbrakk> \<Longrightarrow> cdl.lift (\<box> (dest_sz, unat dest_depth) : target dest_index \<mapsto>u NullCap \<and>* \<box> (src_sz, unat src_depth) : a src_index \<mapsto>u src_cap \<and>* R) sa proof (prove)
goal:
No subgoals!