theory KHeap_DP

lemma decode_cnode_mint_rvu:
  "\<lbrace>\<lambda>s. caps \<noteq> [] \<and>
    cap_has_type src_cap \<and> valid_src_cap src_cap badge
    \<and> ((is_ep_cap src_cap \<or> is_ntfn_cap src_cap) \<longrightarrow>
           cap_badge src_cap = 0)
    \<and> (\<forall>src_cap'. (reset_cap_asid src_cap'
       = reset_cap_asid src_cap) \<longrightarrow>
         (let x = update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap') in
         Q (InsertCall (derived_cap x)
           (cap_object (fst $ the $ get_index caps 0), offset src_index src_sz)
           (cap_object target, offset dest_index dest_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> (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> Q' s  \<rbrace>
      decode_cnode_invocation target target_ref caps
      (CNodeMintIntent dest_index dest_depth src_index src_depth rights badge)
     \<lbrace>\<lambda>rv s. Q rv s\<rbrace>, \<lbrace>\<lambda>r. Q'\<rbrace>" apply (unfold validE_def) apply (rule hoare_name_pre_state) apply (unfold validE_def[symmetric]) apply (clarsimp simp: neq_Nil_conv decode_cnode_invocation_def split_def
                 split: sum.splits) apply (wp derive_cap_invE) apply (wp update_cap_data)+ apply (rule validE_validE_R) 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
    cong:cap_rights_reset_cap_asid
         cap_object_reset_cap_asid) apply (intro conjI) apply (clarsimp simp:user_pointer_at_def Let_def) apply (clarsimp simp:sep_conj_assoc) apply (sep_erule sep_cancel, assumption) apply (clarsimp dest!: mapu_dest_opt_cap
     simp:conj_comms is_exclusive_cap_update_cap_data
     safe_for_derive_not_non valid_src_cap_def) apply (intro conjI impI allI) apply (metis reset_cap_asid_cap_type) apply (frule (1) reset_cap_asid_ep_cap[THEN iffD1]) apply simp apply (metis reset_cap_asid_cap_badge ep_related_capI(1)) apply (frule (1) reset_cap_asid_ntfn_cap[THEN iffD1]) apply simp apply (metis reset_cap_asid_cap_badge ep_related_capI(2)) apply (metis option.inject reset_cap_asid_cnode_cap) apply (metis cap_rights_reset_cap_asid) apply sep_solve done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. caps \<noteq> [] \<and> cap_has_type src_cap \<and> valid_src_cap src_cap badge \<and> (is_ep_cap src_cap \<or> is_ntfn_cap src_cap \<longrightarrow> cap_badge src_cap = 0) \<and> (\<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> (let x = update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap') in Q (InsertCall (derived_cap x) (cap_object (fst $ the $ get_index caps 0), offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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> Q' s\<rbrace> decode_cnode_invocation target target_ref caps (CNodeMintIntent dest_index dest_depth src_index src_depth rights badge) \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r. Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. caps \<noteq> [] \<and> cap_has_type src_cap \<and> valid_src_cap src_cap badge \<and> (is_ep_cap src_cap \<or> is_ntfn_cap src_cap \<longrightarrow> cap_badge src_cap = 0) \<and> (\<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> (let x = update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap') in Q (InsertCall (derived_cap x) (cap_object (fst $ the $ get_index caps 0), offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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> Q' s\<rbrace> decode_cnode_invocation target target_ref caps (CNodeMintIntent dest_index dest_depth src_index src_depth rights badge) \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' s | Inr r \<Rightarrow> Q r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. caps \<noteq> [] \<and> cap_has_type src_cap \<and> valid_src_cap src_cap badge \<and> (is_ep_cap src_cap \<or> is_ntfn_cap src_cap \<longrightarrow> cap_badge src_cap = 0) \<and> (\<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> (let x = update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap') in Q (InsertCall (derived_cap x) (cap_object (fst $ the $ get_index caps 0), offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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> Q' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_cnode_invocation target target_ref caps (CNodeMintIntent dest_index dest_depth src_index src_depth rights badge) \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' s | Inr r \<Rightarrow> Q r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. caps \<noteq> [] \<and> cap_has_type src_cap \<and> valid_src_cap src_cap badge \<and> (is_ep_cap src_cap \<or> is_ntfn_cap src_cap \<longrightarrow> cap_badge src_cap = 0) \<and> (\<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> (let x = update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap') in Q (InsertCall (derived_cap x) (cap_object (fst $ the $ get_index caps 0), offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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> Q' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_cnode_invocation target target_ref caps (CNodeMintIntent dest_index dest_depth src_index src_depth rights badge) \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ys type. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<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);
new_cap' <- liftE (update_cap_data False badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap));
cap <- derive_cap src_slot new_cap';
y <- whenE (cap = NullCap) throw;
returnOk (InsertCall cap src_slot dest_slot)
odE \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>s a aa b ys type p dest_slot y src_slot src_capa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?B26 s a aa b ys type p dest_slot y src_slot src_capa\<rbrace> update_cap_data False badge (update_cap_rights (cap_rights src_capa \<inter> rights) src_capa) \<lbrace>\<lambda>new_cap' s. (if derived_cap new_cap' = NullCap then \<lambda>s. Q' s \<and> True else Q (InsertCall (derived_cap new_cap') src_slot dest_slot)) s \<and> Q' s\<rbrace>
 2. \<And>s a aa b ys type p dest_slot y src_slot. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?B25 s a aa b ys type p dest_slot y src_slot\<rbrace> liftE (get_cap src_slot) \<lbrace>?B26 s a aa b ys type p dest_slot y src_slot\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 3. \<And>s a aa b ys type p dest_slot y. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?B24 s a aa b ys type p dest_slot y\<rbrace> lookup_slot_for_cnode_op (fst p) src_index (unat src_depth) \<lbrace>?B25 s a aa b ys type p dest_slot y\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 4. \<And>s a aa b ys type p dest_slot. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?B23 s a aa b ys type p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>?B24 s a aa b ys type p dest_slot\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 5. \<And>s a aa b ys type p. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s a aa b ys type p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B23 s a aa b ys type p\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 6. \<And>s a aa b ys type. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 s a aa b ys type\<rbrace> throw_on_none (get_index ((a, aa, b) # ys) 0) \<lbrace>?B22 s a aa b ys type\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 7. \<And>s a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s; s = sa\<rbrakk> \<Longrightarrow> ?Q21 s a aa b ys type sa proof (prove)
goal (5 subgoals):
 1. \<And>s a aa b ys type p dest_slot y. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'47 s a aa b ys type 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 (update_cap_rights (cap_rights (the (opt_cap src_slot s)) \<inter> rights) (the (opt_cap src_slot s))) badge \<and> cap_has_type (update_cap_rights (cap_rights (the (opt_cap src_slot s)) \<inter> rights) (the (opt_cap src_slot s))) \<and> (is_ep_cap (update_cap_rights (cap_rights (the (opt_cap src_slot s)) \<inter> rights) (the (opt_cap src_slot s))) \<or> is_ntfn_cap (update_cap_rights (cap_rights (the (opt_cap src_slot s)) \<inter> rights) (the (opt_cap src_slot s))) \<longrightarrow> \<not> False \<and> cap_badge (update_cap_rights (cap_rights (the (opt_cap src_slot s)) \<inter> rights) (the (opt_cap src_slot s))) = 0) \<and> (if derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights (the (opt_cap src_slot s)) \<inter> rights) (the (opt_cap src_slot s)))) = NullCap then \<lambda>s. Q' s \<and> True else Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights (the (opt_cap src_slot s)) \<inter> rights) (the (opt_cap src_slot s))))) src_slot dest_slot)) s \<and> Q' s\<rbrace>, -
 2. \<And>s a aa b ys type p dest_slot. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?B23 s a aa b ys type p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>\<lambda>y sa. Q' sa \<and> ?P'47 s a aa b ys type p dest_slot y sa\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 3. \<And>s a aa b ys type p. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s a aa b ys type p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B23 s a aa b ys type p\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 4. \<And>s a aa b ys type. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 s a aa b ys type\<rbrace> throw_on_none (get_index ((a, aa, b) # ys) 0) \<lbrace>?B22 s a aa b ys type\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 5. \<And>s a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s; s = sa\<rbrakk> \<Longrightarrow> ?Q21 s a aa b ys type sa proof (prove)
goal (5 subgoals):
 1. \<And>s a aa b ys type p dest_slot y. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'47 s a aa b ys type 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 (update_cap_rights (cap_rights (the (opt_cap src_slot s)) \<inter> rights) (the (opt_cap src_slot s))) badge \<and> cap_has_type (update_cap_rights (cap_rights (the (opt_cap src_slot s)) \<inter> rights) (the (opt_cap src_slot s))) \<and> (is_ep_cap (update_cap_rights (cap_rights (the (opt_cap src_slot s)) \<inter> rights) (the (opt_cap src_slot s))) \<or> is_ntfn_cap (update_cap_rights (cap_rights (the (opt_cap src_slot s)) \<inter> rights) (the (opt_cap src_slot s))) \<longrightarrow> \<not> False \<and> cap_badge (update_cap_rights (cap_rights (the (opt_cap src_slot s)) \<inter> rights) (the (opt_cap src_slot s))) = 0) \<and> (if derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights (the (opt_cap src_slot s)) \<inter> rights) (the (opt_cap src_slot s)))) = NullCap then \<lambda>s. Q' s \<and> True else Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights (the (opt_cap src_slot s)) \<inter> rights) (the (opt_cap src_slot s))))) src_slot dest_slot)) s \<and> Q' s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s a aa b ys type p dest_slot. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?B23 s a aa b ys type p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>\<lambda>y sa. Q' sa \<and> ?P'47 s a aa b ys type p dest_slot y sa\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 3. \<And>s a aa b ys type p. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s a aa b ys type p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B23 s a aa b ys type p\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 4. \<And>s a aa b ys type. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 s a aa b ys type\<rbrace> throw_on_none (get_index ((a, aa, b) # ys) 0) \<lbrace>?B22 s a aa b ys type\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 5. \<And>s a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s; s = sa\<rbrakk> \<Longrightarrow> ?Q21 s a aa b ys type sa proof (prove)
goal (5 subgoals):
 1. \<And>s a aa b ys type p dest_slot. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?P'47 s a aa b ys type 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 (update_cap_rights (cap_rights (the (opt_cap src_slot s)) \<inter> rights) (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)) \<longrightarrow> cap_badge (the (opt_cap src_slot s)) = 0) \<and> (is_ntfn_cap (the (opt_cap src_slot s)) \<longrightarrow> cap_badge (the (opt_cap src_slot s)) = 0) \<and> (derived_cap (the (opt_cap src_slot s)) = NullCap \<longrightarrow> Q' s) \<and> (derived_cap (the (opt_cap src_slot s)) \<noteq> NullCap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights (the (opt_cap src_slot s)) \<inter> rights) (the (opt_cap src_slot s))))) src_slot dest_slot) s) \<and> Q' s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s a aa b ys type p dest_slot. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?B23 s a aa b ys type p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>\<lambda>y sa. Q' sa \<and> ?P'47 s a aa b ys type p dest_slot y sa\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 3. \<And>s a aa b ys type p. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s a aa b ys type p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B23 s a aa b ys type p\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 4. \<And>s a aa b ys type. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 s a aa b ys type\<rbrace> throw_on_none (get_index ((a, aa, b) # ys) 0) \<lbrace>?B22 s a aa b ys type\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 5. \<And>s a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s; s = sa\<rbrakk> \<Longrightarrow> ?Q21 s a aa b ys type sa proof (prove)
goal (4 subgoals):
 1. \<And>s a aa b ys type p dest_slot. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?B23 s a aa b ys type p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>\<lambda>y s. Q' s \<and> ((\<exists>y. opt_cap (cap_object (fst p), offset src_index src_sz) s = Some y) \<longrightarrow> valid_src_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<inter> rights) (the (opt_cap (cap_object (fst p), offset src_index src_sz) s))) badge \<and> cap_has_type (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<and> (is_ep_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<longrightarrow> cap_badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) = 0) \<and> (is_ntfn_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<longrightarrow> cap_badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) = 0) \<and> (derived_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) = NullCap \<longrightarrow> Q' s) \<and> (derived_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<noteq> NullCap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<inter> rights) (the (opt_cap (cap_object (fst p), offset src_index src_sz) s))))) (cap_object (fst p), offset src_index src_sz) dest_slot) s) \<and> Q' s) \<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) s\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 2. \<And>s a aa b ys type p. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s a aa b ys type p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B23 s a aa b ys type p\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 3. \<And>s a aa b ys type. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 s a aa b ys type\<rbrace> throw_on_none (get_index ((a, aa, b) # ys) 0) \<lbrace>?B22 s a aa b ys type\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 4. \<And>s a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s; s = sa\<rbrakk> \<Longrightarrow> ?Q21 s a aa b ys type sa proof (prove)
goal (4 subgoals):
 1. \<And>s a aa b ys type p dest_slot. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?B23 s a aa b ys type p dest_slot\<rbrace> ensure_empty dest_slot \<lbrace>\<lambda>y s. Q' s \<and> ((\<exists>y. opt_cap (cap_object (fst p), offset src_index src_sz) s = Some y) \<longrightarrow> valid_src_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<inter> rights) (the (opt_cap (cap_object (fst p), offset src_index src_sz) s))) badge \<and> cap_has_type (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<and> (is_ep_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<longrightarrow> cap_badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) = 0) \<and> (is_ntfn_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<longrightarrow> cap_badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) = 0) \<and> (derived_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) = NullCap \<longrightarrow> Q' s) \<and> (derived_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<noteq> NullCap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<inter> rights) (the (opt_cap (cap_object (fst p), offset src_index src_sz) s))))) (cap_object (fst p), offset src_index src_sz) dest_slot) s) \<and> Q' s) \<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) s\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 2. \<And>s a aa b ys type p. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s a aa b ys type p\<rbrace> lookup_slot_for_cnode_op target dest_index (unat dest_depth) \<lbrace>?B23 s a aa b ys type p\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 3. \<And>s a aa b ys type. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 s a aa b ys type\<rbrace> throw_on_none (get_index ((a, aa, b) # ys) 0) \<lbrace>?B22 s a aa b ys type\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 4. \<And>s a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s; s = sa\<rbrakk> \<Longrightarrow> ?Q21 s a aa b ys type sa proof (prove)
goal (3 subgoals):
 1. \<And>s a aa b ys type p. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?B22 s a aa b ys type 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>* ?R56 s a aa b ys type p dest_slot) and (\<lambda>s. Q' s \<and> ((\<exists>y. opt_cap (cap_object (fst p), offset src_index src_sz) s = Some y) \<longrightarrow> valid_src_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<inter> rights) (the (opt_cap (cap_object (fst p), offset src_index src_sz) s))) badge \<and> cap_has_type (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<and> (is_ep_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<longrightarrow> cap_badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) = 0) \<and> (is_ntfn_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<longrightarrow> cap_badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) = 0) \<and> (derived_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) = NullCap \<longrightarrow> Q' s) \<and> (derived_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<noteq> NullCap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<inter> rights) (the (opt_cap (cap_object (fst p), offset src_index src_sz) s))))) (cap_object (fst p), offset src_index src_sz) dest_slot) s) \<and> Q' s) \<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) s)\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 2. \<And>s a aa b ys type. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 s a aa b ys type\<rbrace> throw_on_none (get_index ((a, aa, b) # ys) 0) \<lbrace>?B22 s a aa b ys type\<rbrace>, \<lbrace>\<lambda>e. Q'\<rbrace>
 3. \<And>s a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s; s = sa\<rbrakk> \<Longrightarrow> ?Q21 s a aa b ys type sa proof (prove)
goal (2 subgoals):
 1. \<And>s a aa b ys type. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 s a aa b ys type\<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>* ?R56 s a aa b ys type p (cap_object target, offset dest_index dest_sz)) and (\<lambda>s. Q' s \<and> ((\<exists>y. opt_cap (cap_object (fst p), offset src_index src_sz) s = Some y) \<longrightarrow> valid_src_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<inter> rights) (the (opt_cap (cap_object (fst p), offset src_index src_sz) s))) badge \<and> cap_has_type (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<and> (is_ep_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<longrightarrow> cap_badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) = 0) \<and> (is_ntfn_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<longrightarrow> cap_badge (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) = 0) \<and> (derived_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) = NullCap \<longrightarrow> Q' s) \<and> (derived_cap (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<noteq> NullCap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights (the (opt_cap (cap_object (fst p), offset src_index src_sz) s)) \<inter> rights) (the (opt_cap (cap_object (fst p), offset src_index src_sz) s))))) (cap_object (fst p), offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) s) \<and> Q' s) \<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) s)) 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>\<lambda>e. Q'\<rbrace>
 2. \<And>s a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s; s = sa\<rbrakk> \<Longrightarrow> ?Q21 s a aa b ys type sa proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) 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; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; 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; Q' s; 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>* ?R56 s a aa b ys type y (cap_object target, offset dest_index dest_sz)) sa \<and> Q' sa \<and> ((\<exists>ya. opt_cap (cap_object (fst y), offset src_index src_sz) sa = Some ya) \<longrightarrow> valid_src_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object (fst y), offset src_index src_sz) sa)) \<inter> rights) (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> (is_ep_cap (the (opt_cap (cap_object (fst y), offset src_index src_sz) sa)) \<longrightarrow> cap_badge (the (opt_cap (cap_object (fst y), offset src_index src_sz) sa)) = 0) \<and> (is_ntfn_cap (the (opt_cap (cap_object (fst y), offset src_index src_sz) sa)) \<longrightarrow> cap_badge (the (opt_cap (cap_object (fst y), offset src_index src_sz) sa)) = 0) \<and> (derived_cap (the (opt_cap (cap_object (fst y), offset src_index src_sz) sa)) = NullCap \<longrightarrow> Q' sa) \<and> (derived_cap (the (opt_cap (cap_object (fst y), offset src_index src_sz) sa)) \<noteq> NullCap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights (the (opt_cap (cap_object (fst y), offset src_index src_sz) sa)) \<inter> rights) (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> Q' 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>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<rbrakk> \<Longrightarrow> cdl.lift ((cap_object target, offset dest_index dest_sz) \<mapsto>c NullCap \<and>* ?R56 sa a aa b ys type (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 (update_cap_rights (cap_rights (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<inter> rights) (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> (is_ep_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<longrightarrow> cap_badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) = 0) \<and> (is_ntfn_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<longrightarrow> cap_badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) = 0) \<and> (derived_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> NullCap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<inter> rights) (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>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<rbrakk> \<Longrightarrow> cdl.lift ((cap_object target, offset dest_index dest_sz) \<mapsto>c NullCap \<and>* ?R56 sa a aa b ys type (a, aa, b) (cap_object target, offset dest_index dest_sz)) sa
 2. \<And>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<rbrakk> \<Longrightarrow> (\<exists>y. opt_cap (cap_object a, offset src_index src_sz) sa = Some y) \<longrightarrow> valid_src_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<inter> rights) (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> (is_ep_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<longrightarrow> cap_badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) = 0) \<and> (is_ntfn_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<longrightarrow> cap_badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) = 0) \<and> (derived_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> NullCap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<inter> rights) (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>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<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>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; 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>* ?R56 sa a aa b ys type (a, aa, b) (cap_object target, offset dest_index dest_sz)) sa
 2. \<And>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<rbrakk> \<Longrightarrow> (\<exists>y. opt_cap (cap_object a, offset src_index src_sz) sa = Some y) \<longrightarrow> valid_src_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<inter> rights) (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> (is_ep_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<longrightarrow> cap_badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) = 0) \<and> (is_ntfn_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<longrightarrow> cap_badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) = 0) \<and> (derived_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> NullCap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<inter> rights) (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>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<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>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; 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>* ?R56 sa a aa b ys type (a, aa, b) (cap_object target, offset dest_index dest_sz)) sa
 2. \<And>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<rbrakk> \<Longrightarrow> (\<exists>y. opt_cap (cap_object a, offset src_index src_sz) sa = Some y) \<longrightarrow> valid_src_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<inter> rights) (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> (is_ep_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<longrightarrow> cap_badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) = 0) \<and> (is_ntfn_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<longrightarrow> cap_badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) = 0) \<and> (derived_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> NullCap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<inter> rights) (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>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<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>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<rbrakk> \<Longrightarrow> (\<exists>y. opt_cap (cap_object a, offset src_index src_sz) sa = Some y) \<longrightarrow> valid_src_cap (update_cap_rights (cap_rights (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<inter> rights) (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> (is_ep_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<longrightarrow> cap_badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) = 0) \<and> (is_ntfn_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<longrightarrow> cap_badge (the (opt_cap (cap_object a, offset src_index src_sz) sa)) = 0) \<and> (derived_cap (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<noteq> NullCap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights (the (opt_cap (cap_object a, offset src_index src_sz) sa)) \<inter> rights) (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>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<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>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'\<rbrakk> \<Longrightarrow> cap_has_type cap' \<and> (is_ep_cap cap' \<longrightarrow> cap_badge cap' = 0) \<and> (is_ntfn_cap cap' \<longrightarrow> cap_badge cap' = 0) \<and> (is_cnode_cap cap' \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size cap' \<le> word_bits) \<and> (derived_cap cap' \<noteq> NullCap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights cap' \<inter> rights) cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa)
 2. \<And>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<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 (6 subgoals):
 1. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'\<rbrakk> \<Longrightarrow> cap_has_type cap'
 2. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_ep_cap cap'\<rbrakk> \<Longrightarrow> cap_badge cap' = 0
 3. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_ntfn_cap cap'\<rbrakk> \<Longrightarrow> cap_badge cap' = 0
 4. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_cnode_cap cap'\<rbrakk> \<Longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size cap' \<le> word_bits
 5. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; derived_cap cap' \<noteq> NullCap\<rbrakk> \<Longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights cap' \<inter> rights) cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa
 6. \<And>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<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 (5 subgoals):
 1. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_ep_cap cap'\<rbrakk> \<Longrightarrow> cap_badge cap' = 0
 2. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_ntfn_cap cap'\<rbrakk> \<Longrightarrow> cap_badge cap' = 0
 3. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_cnode_cap cap'\<rbrakk> \<Longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size cap' \<le> word_bits
 4. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; derived_cap cap' \<noteq> NullCap\<rbrakk> \<Longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights cap' \<inter> rights) cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa
 5. \<And>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<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 (5 subgoals):
 1. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_ep_cap cap'; is_ep_cap src_cap\<rbrakk> \<Longrightarrow> cap_badge cap' = 0
 2. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_ntfn_cap cap'\<rbrakk> \<Longrightarrow> cap_badge cap' = 0
 3. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_cnode_cap cap'\<rbrakk> \<Longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size cap' \<le> word_bits
 4. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; derived_cap cap' \<noteq> NullCap\<rbrakk> \<Longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights cap' \<inter> rights) cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa
 5. \<And>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<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 (5 subgoals):
 1. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; EndpointType = type; cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_ep_cap cap'; is_ep_cap src_cap\<rbrakk> \<Longrightarrow> cap_badge cap' = 0
 2. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_ntfn_cap cap'\<rbrakk> \<Longrightarrow> cap_badge cap' = 0
 3. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_cnode_cap cap'\<rbrakk> \<Longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size cap' \<le> word_bits
 4. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; derived_cap cap' \<noteq> NullCap\<rbrakk> \<Longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights cap' \<inter> rights) cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa
 5. \<And>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<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 (4 subgoals):
 1. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_ntfn_cap cap'\<rbrakk> \<Longrightarrow> cap_badge cap' = 0
 2. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_cnode_cap cap'\<rbrakk> \<Longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size cap' \<le> word_bits
 3. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; derived_cap cap' \<noteq> NullCap\<rbrakk> \<Longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights cap' \<inter> rights) cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa
 4. \<And>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<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 (4 subgoals):
 1. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_ntfn_cap cap'; is_ntfn_cap src_cap\<rbrakk> \<Longrightarrow> cap_badge cap' = 0
 2. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_cnode_cap cap'\<rbrakk> \<Longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size cap' \<le> word_bits
 3. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; derived_cap cap' \<noteq> NullCap\<rbrakk> \<Longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights cap' \<inter> rights) cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa
 4. \<And>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<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 (4 subgoals):
 1. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; NotificationType = type; cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_ntfn_cap cap'; is_ntfn_cap src_cap\<rbrakk> \<Longrightarrow> cap_badge cap' = 0
 2. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_cnode_cap cap'\<rbrakk> \<Longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size cap' \<le> word_bits
 3. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; derived_cap cap' \<noteq> NullCap\<rbrakk> \<Longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights cap' \<inter> rights) cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa
 4. \<And>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<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>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; is_cnode_cap cap'\<rbrakk> \<Longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size cap' \<le> word_bits
 2. \<And>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; derived_cap cap' \<noteq> NullCap\<rbrakk> \<Longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights cap' \<inter> rights) cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa
 3. \<And>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<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>a aa b ys type sa cap'. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; type = CNodeType \<longrightarrow> unat ((badge >> 3) && mask 5) + cnode_cap_size src_cap \<le> word_bits; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa; unat src_depth \<le> word_bits; 0 < unat src_depth; unat dest_depth \<le> word_bits; 0 < unat dest_depth; Q' sa; reset_cap_asid cap' = reset_cap_asid src_cap; opt_cap (cap_object a, offset src_index src_sz) sa = Some cap'; derived_cap cap' \<noteq> NullCap\<rbrakk> \<Longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights cap' \<inter> rights) cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_sz)) sa
 2. \<And>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<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>a aa b ys type sa. \<lbrakk>caps = (a, aa, b) # ys; cap_type src_cap = Some type; valid_src_cap src_cap badge; type = EndpointType \<longrightarrow> cap_badge src_cap = 0; type = NotificationType \<longrightarrow> cap_badge src_cap = 0; \<forall>src_cap'. reset_cap_asid src_cap' = reset_cap_asid src_cap \<longrightarrow> Q (InsertCall (derived_cap (update_cap_data_det badge (update_cap_rights (cap_rights src_cap \<inter> rights) src_cap'))) (cap_object a, offset src_index src_sz) (cap_object target, offset dest_index dest_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> (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; Q' sa\<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!