theory CNode_DR

lemma lookup_slot_for_cnode_op_corres:
  "\<lbrakk> idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap;depth = depth'  \<rbrakk> \<Longrightarrow>
  dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p'))
    \<top>
    (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs)
    (CSpace_D.lookup_slot_for_cnode_op cnode_cap' idx depth)
    (CSpace_A.lookup_slot_for_cnode_op b cnode_cap idx' depth')" apply (simp add: CSpace_D.lookup_slot_for_cnode_op_def
                   CSpace_A.lookup_slot_for_cnode_op_def
                   cdl_resolve_address_bits_error_branch1) apply (rule conjI) prefer 2 apply (cases "depth = 0 \<or> word_bits < depth", simp) apply (simp add: fault_to_except_def throw_handle) apply (clarsimp simp: word_bits_def) apply (rule whenE_throwError_corres_initial, simp, rule refl) apply (simp add: fault_to_except_def lookup_error_on_failure_def) apply (rule corres_handle2') apply (rule corres_initial_splitE [where Q="\<lambda>_. \<top>" and Q'="\<lambda>_. \<top>"]) apply (rule corres_handle2) apply (subst cdl_resolve_address_bits_eq [rule_format]) prefer 2 apply (rule resolve_address_bits_corres) apply simp apply (rule refl) apply clarsimp apply simp apply clarsimp apply (rule conjI) apply clarsimp apply (rule corres_returnOk, rule refl) apply (clarsimp simp: neq_Nil_conv) apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.lookup_slot_for_cnode_op cnode_cap' idx depth) (CSpace_A.lookup_slot_for_cnode_op b cnode_cap idx' depth') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'\<rbrakk> \<Longrightarrow> (Structures_A.is_cnode_cap cnode_cap \<longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs) (doE y <- whenE (depth' = 0 \<or> word_bits < depth') throw;
(slot, rem) <- fault_to_except (CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth');
if rem = 0 then returnOk slot else throw
odE) (doE y <- whenE (depth' = 0 \<or> word_bits < depth') (throwError (RangeError 1 (word_of_nat word_bits)));
lookup_error_on_failure b (doE (slot, rem) <- CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx');
case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0
odE)
odE)) \<and> (\<not> Structures_A.is_cnode_cap cnode_cap \<longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs) (doE y <- whenE (depth' = 0 \<or> word_bits < depth') throw;
(slot, rem) <- fault_to_except throw;
if rem = 0 then returnOk slot else throw
odE) (throwError (FailedLookup b InvalidRoot))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'\<rbrakk> \<Longrightarrow> Structures_A.is_cnode_cap cnode_cap \<longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs) (doE y <- whenE (depth' = 0 \<or> word_bits < depth') throw;
(slot, rem) <- fault_to_except (CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth');
if rem = 0 then returnOk slot else throw
odE) (doE y <- whenE (depth' = 0 \<or> word_bits < depth') (throwError (RangeError 1 (word_of_nat word_bits)));
lookup_error_on_failure b (doE (slot, rem) <- CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx');
case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0
odE)
odE)
 2. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'\<rbrakk> \<Longrightarrow> \<not> Structures_A.is_cnode_cap cnode_cap \<longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs) (doE y <- whenE (depth' = 0 \<or> word_bits < depth') throw;
(slot, rem) <- fault_to_except throw;
if rem = 0 then returnOk slot else throw
odE) (throwError (FailedLookup b InvalidRoot)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'\<rbrakk> \<Longrightarrow> \<not> Structures_A.is_cnode_cap cnode_cap \<longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs) (doE y <- whenE (depth' = 0 \<or> word_bits < depth') throw;
(slot, rem) <- fault_to_except throw;
if rem = 0 then returnOk slot else throw
odE) (throwError (FailedLookup b InvalidRoot))
 2. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'\<rbrakk> \<Longrightarrow> Structures_A.is_cnode_cap cnode_cap \<longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs) (doE y <- whenE (depth' = 0 \<or> word_bits < depth') throw;
(slot, rem) <- fault_to_except (CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth');
if rem = 0 then returnOk slot else throw
odE) (doE y <- whenE (depth' = 0 \<or> word_bits < depth') (throwError (RangeError 1 (word_of_nat word_bits)));
lookup_error_on_failure b (doE (slot, rem) <- CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx');
case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0
odE)
odE) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; \<not> (depth = 0 \<or> word_bits < depth)\<rbrakk> \<Longrightarrow> \<not> Structures_A.is_cnode_cap cnode_cap \<longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs) (doE y <- whenE (depth' = 0 \<or> word_bits < depth') throw;
(slot, rem) <- fault_to_except throw;
if rem = 0 then returnOk slot else throw
odE) (throwError (FailedLookup b InvalidRoot))
 2. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'\<rbrakk> \<Longrightarrow> Structures_A.is_cnode_cap cnode_cap \<longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs) (doE y <- whenE (depth' = 0 \<or> word_bits < depth') throw;
(slot, rem) <- fault_to_except (CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth');
if rem = 0 then returnOk slot else throw
odE) (doE y <- whenE (depth' = 0 \<or> word_bits < depth') (throwError (RangeError 1 (word_of_nat word_bits)));
lookup_error_on_failure b (doE (slot, rem) <- CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx');
case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0
odE)
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'\<rbrakk> \<Longrightarrow> Structures_A.is_cnode_cap cnode_cap \<longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs) (doE y <- whenE (depth' = 0 \<or> word_bits < depth') throw;
(slot, rem) <- fault_to_except (CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth');
if rem = 0 then returnOk slot else throw
odE) (doE y <- whenE (depth' = 0 \<or> word_bits < depth') (throwError (RangeError 1 (word_of_nat word_bits)));
lookup_error_on_failure b (doE (slot, rem) <- CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx');
case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0
odE)
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs) (doE y <- whenE (depth' = 0 \<or> 32 < depth') throw;
(slot, rem) <- fault_to_except (CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth');
if rem = 0 then returnOk slot else throw
odE) (doE y <- whenE (depth' = 0 \<or> 32 < depth') (throwError (RangeError 1 0x20));
lookup_error_on_failure b (doE (slot, rem) <- CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx');
case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0
odE)
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; \<not> (depth' = 0 \<or> 32 < depth')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs) (doE (slot, rem) <- fault_to_except (CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth');
if rem = 0 then returnOk slot else throw
odE) (lookup_error_on_failure b (doE (slot, rem) <- CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx');
case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0
odE)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs) (doE (slot, rem) <- CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth' <handle2> (\<lambda>x. throw);
if rem = 0 then returnOk slot else throw
odE) (doE (slot, rem) <- CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx');
case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0
odE <handle2> throwError \<circ> FailedLookup b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs) (doE (slot, rem) <- CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth' <handle2> (\<lambda>x. throw);
if rem = 0 then returnOk slot else throw
odE) (doE (slot, rem) <- CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx');
case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0
odE) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ?r'21) (\<lambda>_. True) (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth' <handle2> (\<lambda>x. throw)) (CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx'))
 2. \<And>rv rv'. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'; ?r'21 rv rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (\<lambda>_. True) (case rv of (slot, rem) \<Rightarrow> if rem = 0 then returnOk slot else throw) (case rv' of (slot, rem) \<Rightarrow> case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0)
 3. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth' <handle2> (\<lambda>x. throw) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs\<rbrace> CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx') \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ?r'21) (\<lambda>_. True) (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth') (CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx'))
 2. \<And>rv rv'. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'; ?r'21 rv rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (\<lambda>_. True) (case rv of (slot, rem) \<Rightarrow> if rem = 0 then returnOk slot else throw) (case rv' of (slot, rem) \<Rightarrow> case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0)
 3. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth' <handle2> (\<lambda>x. throw) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs\<rbrace> CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx') \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> ?a29 + depth' \<le> length idx' \<and> length idx' \<le> 32
 2. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ?r'21) (\<lambda>_. True) (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl (drop ?a29 idx')) depth') (CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx'))
 3. \<And>rv rv'. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'; ?r'21 rv rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (\<lambda>_. True) (case rv of (slot, rem) \<Rightarrow> if rem = 0 then returnOk slot else throw) (case rv' of (slot, rem) \<Rightarrow> case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0)
 4. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth' <handle2> (\<lambda>x. throw) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 5. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs\<rbrace> CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx') \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ?r'21) (\<lambda>_. True) (valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl (drop ?a29 idx')) depth') (CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx'))
 2. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> ?a29 + depth' \<le> length idx' \<and> length idx' \<le> 32
 3. \<And>rv rv'. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'; ?r'21 rv rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (\<lambda>_. True) (case rv of (slot, rem) \<Rightarrow> if rem = 0 then returnOk slot else throw) (case rv' of (slot, rem) \<Rightarrow> case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0)
 4. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth' <handle2> (\<lambda>x. throw) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 5. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs\<rbrace> CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx') \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> length (drop (32 - depth') idx') \<le> 32
 2. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> transform_cap cnode_cap = transform_cap cnode_cap
 3. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> depth' = length (drop (32 - depth') idx')
 4. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> 32 - depth' + depth' \<le> length idx' \<and> length idx' \<le> 32
 5. \<And>rv rv'. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'; fst rv = transform_cslot_ptr (fst rv') \<and> snd rv = length (snd rv')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (\<lambda>_. True) (case rv of (slot, rem) \<Rightarrow> if rem = 0 then returnOk slot else throw) (case rv' of (slot, rem) \<Rightarrow> case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0)
 6. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth' <handle2> (\<lambda>x. throw) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 7. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs\<rbrace> CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx') \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> transform_cap cnode_cap = transform_cap cnode_cap
 2. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> depth' = length (drop (32 - depth') idx')
 3. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> 32 - depth' + depth' \<le> length idx' \<and> length idx' \<le> 32
 4. \<And>rv rv'. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'; fst rv = transform_cslot_ptr (fst rv') \<and> snd rv = length (snd rv')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (\<lambda>_. True) (case rv of (slot, rem) \<Rightarrow> if rem = 0 then returnOk slot else throw) (case rv' of (slot, rem) \<Rightarrow> case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0)
 5. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth' <handle2> (\<lambda>x. throw) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 6. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs\<rbrace> CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx') \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> depth' = length (drop (32 - depth') idx')
 2. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> 32 - depth' + depth' \<le> length idx' \<and> length idx' \<le> 32
 3. \<And>rv rv'. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'; fst rv = transform_cslot_ptr (fst rv') \<and> snd rv = length (snd rv')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (\<lambda>_. True) (case rv of (slot, rem) \<Rightarrow> if rem = 0 then returnOk slot else throw) (case rv' of (slot, rem) \<Rightarrow> case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0)
 4. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth' <handle2> (\<lambda>x. throw) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 5. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs\<rbrace> CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx') \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> 32 - depth' + depth' \<le> length idx' \<and> length idx' \<le> 32
 2. \<And>rv rv'. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'; fst rv = transform_cslot_ptr (fst rv') \<and> snd rv = length (snd rv')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (\<lambda>_. True) (case rv of (slot, rem) \<Rightarrow> if rem = 0 then returnOk slot else throw) (case rv' of (slot, rem) \<Rightarrow> case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0)
 3. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth' <handle2> (\<lambda>x. throw) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs\<rbrace> CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx') \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'; fst rv = transform_cslot_ptr (fst rv') \<and> snd rv = length (snd rv')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (\<lambda>_. True) (case rv of (slot, rem) \<Rightarrow> if rem = 0 then returnOk slot else throw) (case rv' of (slot, rem) \<Rightarrow> case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0)
 2. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth' <handle2> (\<lambda>x. throw) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 3. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs\<rbrace> CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx') \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>a b aa bb bc. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth'; \<not> 32 < depth'; (a, b) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> (bc = [] \<longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (\<lambda>_. True) (returnOk (transform_cslot_ptr (aa, bb))) (returnOk (aa, bb))) \<and> (bc \<noteq> [] \<longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (\<lambda>_. True) throw (case bc of [] \<Rightarrow> returnOk (aa, bb) | a # list \<Rightarrow> throwError $ DepthMismatch (length bc) 0))
 2. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth' <handle2> (\<lambda>x. throw) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 3. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs\<rbrace> CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx') \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>a b aa bb bc. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth'; \<not> 32 < depth'; (a, b) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> bc = [] \<longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (\<lambda>_. True) (returnOk (transform_cslot_ptr (aa, bb))) (returnOk (aa, bb))
 2. \<And>a b aa bb bc. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth'; \<not> 32 < depth'; (a, b) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> bc \<noteq> [] \<longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (\<lambda>_. True) throw (case bc of [] \<Rightarrow> returnOk (aa, bb) | a # list \<Rightarrow> throwError $ DepthMismatch (length bc) 0)
 3. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth' <handle2> (\<lambda>x. throw) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs\<rbrace> CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx') \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>a b aa bb. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth'; \<not> 32 < depth'; (a, b) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (\<lambda>_. True) (returnOk (transform_cslot_ptr (aa, bb))) (returnOk (aa, bb))
 2. \<And>a b aa bb bc. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth'; \<not> 32 < depth'; (a, b) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> bc \<noteq> [] \<longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (\<lambda>_. True) throw (case bc of [] \<Rightarrow> returnOk (aa, bb) | a # list \<Rightarrow> throwError $ DepthMismatch (length bc) 0)
 3. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth' <handle2> (\<lambda>x. throw) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 4. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs\<rbrace> CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx') \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>a b aa bb bc. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth'; \<not> 32 < depth'; (a, b) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> bc \<noteq> [] \<longrightarrow> dcorres (dc \<oplus> (\<lambda>p p'. p = transform_cslot_ptr p')) (\<lambda>_. True) (\<lambda>_. True) throw (case bc of [] \<Rightarrow> returnOk (aa, bb) | a # list \<Rightarrow> throwError $ DepthMismatch (length bc) 0)
 2. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth' <handle2> (\<lambda>x. throw) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 3. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs\<rbrace> CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx') \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_D.resolve_address_bits (transform_cap cnode_cap) (of_bl idx') depth' <handle2> (\<lambda>x. throw) \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>
 2. \<lbrakk>idx = of_bl idx'; length idx' = 32; cnode_cap' = transform_cap cnode_cap; depth = depth'; Structures_A.is_cnode_cap cnode_cap; 0 < depth' \<and> \<not> 32 < depth'\<rbrakk> \<Longrightarrow> \<lbrace>valid_objs and valid_cap cnode_cap and valid_global_refs and valid_idle and valid_etcbs\<rbrace> CSpace_A.resolve_address_bits (cnode_cap, drop (32 - depth') idx') \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace> proof (prove)
goal:
No subgoals!