theory KHeap_DR

lemma resolve_address_bits_terminate_corres:
  "\<lbrakk>in_terminate_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; cap'=transform_cap cap; valid_cap cap s;valid_idle s;length ref \<le> 32;valid_objs s\<rbrakk>
      \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) \<top> ((=) s)
    ( CSpace_D.resolve_address_bits cap' (of_bl ref) (length ref) )
    ( CSpace_A.resolve_address_bits (cap,ref) )" apply (subst KHeap_DR.resolve_address_bits.simps,frule resolve_address_bits_terminate_branch[where 'a=det_ext],fastforce) apply (clarsimp simp:in_terminate_branch_def) apply (clarsimp simp:unlessE_def cap_type_simps assertE_def) apply (subgoal_tac "(of_bl ref >> radix_bits) && mask (length guard) = of_bl guard") apply (clarsimp | rule conjI)+ apply (clarsimp simp:get_cnode_def bind_assoc liftE_bindE) apply (clarsimp simp:valid_cap_def obj_at_def is_cap_table_def) apply (clarsimp split:Structures_A.kernel_object.splits) apply (rename_tac "fun") apply (rule dcorres_expand_pfx) apply clarsimp apply (rule_tac Q="\<lambda>x y. y = (transform s) \<and> x = (transform_object (machine_state s) oref etcb_opt (kernel_object.CNode radix_bits fun))" in corres_symb_exec_l) apply (rule dcorres_expand_pfx) apply (simp split: nat.splits) apply (clarsimp simp: returnOk_def return_def corres_underlying_def transform_cslot_ptr_def) apply (simp only: unat_def) apply (subst eq_nat_nat_iff) apply (simp add:bl_to_bin_ge0)+ apply (subst to_bl_bin[symmetric]) apply (subst bl_and_mask) apply (simp add:word_rep_drop bl_to_bin_rep_F) apply ((drule (1) transform_objects_cnode;
               clarsimp simp: gets_the_def gets_def get_def bind_def return_def valid_def
                              exs_valid_def assert_opt_def transform_def
                       split: nat.splits)+)[3] apply fastforce apply (frule_tac cref1=ref and cref'1="of_bl ref::word32" in iffD2[OF guard_mask_shift,rotated]) apply (simp add: word_rep_drop)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>in_terminate_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; cap' = transform_cap cap; s \<turnstile> cap; valid_idle s; length ref \<le> 32; valid_objs s\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (CSpace_D.resolve_address_bits cap' (of_bl ref) (length ref)) (CSpace_A.resolve_address_bits (cap, ref)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>in_terminate_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; cap' = transform_cap cap; s \<turnstile> cap; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap, ref) = returnOk ((oref, drop (length guard) ref), [])\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE unlessE (Types_D.is_cnode_cap cap') $ throw;
cnode <- liftE $ get_cnode $ cap_object cap';
radix_size <- returnOk $ cdl_cnode_size_bits cnode;
guard_size <- returnOk $ cap_guard_size cap';
cap_guard <- returnOk $ cap_guard cap';
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl ref >> length ref - guard_size) && mask guard_size;
unlessE (guard_size \<le> length ref \<and> guard = cap_guard) $ throw;
whenE (length ref < level_size) $ throw;
offset <- returnOk $ (of_bl ref >> length ref - level_size) && mask radix_size;
slot <- returnOk (cap_object cap', unat offset);
size_left <- returnOk (length ref - level_size);
if size_left = 0 then returnOk (slot, 0) else doE next_cap <- liftE $ KHeap_D.get_cap slot;
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl ref) size_left else returnOk (slot, size_left)
odE
odE) (CSpace_A.resolve_address_bits (cap, ref)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
y <- unlessE ((of_bl ref >> radix_bits) && mask (length guard) = of_bl guard) throw;
y <- whenE (radix_bits < cdl_cnode_size_bits cnode) throw;
if radix_bits \<le> cdl_cnode_size_bits cnode then returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), 0) else doE next_cap <- liftE $ KHeap_D.get_cap (oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode)));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl ref) (radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard))
odE
odE) (returnOk ((oref, drop (length guard) ref), [])) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> ((of_bl ref >> radix_bits) && mask (length guard) = of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
y <- whenE (radix_bits < cdl_cnode_size_bits cnode) throw;
if radix_bits \<le> cdl_cnode_size_bits cnode then returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), 0) else doE next_cap <- liftE $ KHeap_D.get_cap (oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode)));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl ref) (radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard))
odE
odE) (returnOk ((oref, drop (length guard) ref), []))) \<and> ((of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> ((of_bl ref >> radix_bits) && mask (length guard) = of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
y <- whenE (radix_bits < cdl_cnode_size_bits cnode) throw;
if radix_bits \<le> cdl_cnode_size_bits cnode then returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), 0) else doE next_cap <- liftE $ KHeap_D.get_cap (oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode)));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl ref) (radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard))
odE
odE) (returnOk ((oref, drop (length guard) ref), []))) \<and> ((of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), [])))
 2. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
y <- whenE (radix_bits < cdl_cnode_size_bits cnode) throw;
if radix_bits \<le> cdl_cnode_size_bits cnode then returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), 0) else doE next_cap <- liftE $ KHeap_D.get_cap (oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode)));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl ref) (radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard))
odE
odE) (returnOk ((oref, drop (length guard) ref), []))
 2. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))
 3. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (do x <- KHeap_D.get_object oref;
cnode <- case x of cdl_object.CNode x \<Rightarrow> return x | _ \<Rightarrow> fail;
doE y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
y <- whenE (radix_bits < cdl_cnode_size_bits cnode) throw;
if radix_bits \<le> cdl_cnode_size_bits cnode then returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), 0) else doE next_cap <- liftE $ KHeap_D.get_cap (oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode)));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl ref) (radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard))
odE
odE
od) (returnOk ((oref, drop (length guard) ref), []))
 2. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))
 3. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (3 subgoals):
 1. \<And>ko. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some ko; case ko of kernel_object.CNode sz cs \<Rightarrow> radix_bits = sz \<and> well_formed_cnode_n radix_bits cs | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (do x <- KHeap_D.get_object oref;
cnode <- case x of cdl_object.CNode x \<Rightarrow> return x | _ \<Rightarrow> fail;
doE y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
y <- whenE (radix_bits < cdl_cnode_size_bits cnode) throw;
if radix_bits \<le> cdl_cnode_size_bits cnode then returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), 0) else doE next_cap <- liftE $ KHeap_D.get_cap (oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode)));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl ref) (radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard))
odE
odE
od) (returnOk ((oref, drop (length guard) ref), []))
 2. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))
 3. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (3 subgoals):
 1. \<And>x12. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits x12); well_formed_cnode_n radix_bits x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (do x <- KHeap_D.get_object oref;
cnode <- case x of cdl_object.CNode x \<Rightarrow> return x | _ \<Rightarrow> fail;
doE y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
y <- whenE (radix_bits < cdl_cnode_size_bits cnode) throw;
if radix_bits \<le> cdl_cnode_size_bits cnode then returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), 0) else doE next_cap <- liftE $ KHeap_D.get_cap (oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode)));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl ref) (radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard))
odE
odE
od) (returnOk ((oref, drop (length guard) ref), []))
 2. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))
 3. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (3 subgoals):
 1. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (do x <- KHeap_D.get_object oref;
cnode <- case x of cdl_object.CNode x \<Rightarrow> return x | _ \<Rightarrow> fail;
doE y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
y <- whenE (radix_bits < cdl_cnode_size_bits cnode) throw;
if radix_bits \<le> cdl_cnode_size_bits cnode then returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), 0) else doE next_cap <- liftE $ KHeap_D.get_cap (oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode)));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl ref) (radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard))
odE
odE
od) (returnOk ((oref, drop (length guard) ref), []))
 2. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))
 3. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (3 subgoals):
 1. \<And>fun sa s'. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; sa = transform s'; True; s = s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) ((=) sa) ((=) s') (do x <- KHeap_D.get_object oref;
cnode <- case x of cdl_object.CNode x \<Rightarrow> return x | _ \<Rightarrow> fail;
doE y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
y <- whenE (radix_bits < cdl_cnode_size_bits cnode) throw;
if radix_bits \<le> cdl_cnode_size_bits cnode then returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), 0) else doE next_cap <- liftE $ KHeap_D.get_cap (oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode)));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl ref) (radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard))
odE
odE
od) (returnOk ((oref, drop (length guard) ref), []))
 2. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))
 3. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (3 subgoals):
 1. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) ((=) (transform s)) ((=) s) (do x <- KHeap_D.get_object oref;
cnode <- case x of cdl_object.CNode x \<Rightarrow> return x | _ \<Rightarrow> fail;
doE y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
y <- whenE (radix_bits < cdl_cnode_size_bits cnode) throw;
if radix_bits \<le> cdl_cnode_size_bits cnode then returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), 0) else doE next_cap <- liftE $ KHeap_D.get_cap (oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode)));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl ref) (radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard))
odE
odE
od) (returnOk ((oref, drop (length guard) ref), []))
 2. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))
 3. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (6 subgoals):
 1. \<And>fun rv. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>y. y = transform s \<and> rv = transform_object (machine_state s) oref etcb_opt (kernel_object.CNode radix_bits fun)) ((=) s) (do cnode <- case rv of cdl_object.CNode x \<Rightarrow> return x | _ \<Rightarrow> fail;
doE y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
y <- whenE (radix_bits < cdl_cnode_size_bits cnode) throw;
if radix_bits \<le> cdl_cnode_size_bits cnode then returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), 0) else doE next_cap <- liftE $ KHeap_D.get_cap (oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode)));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl ref) (radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard))
odE
odE
od) (returnOk ((oref, drop (length guard) ref), []))
 2. \<And>fun sa. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; transform s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> KHeap_D.get_object oref \<exists>\<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s)\<rbrace> KHeap_D.get_object oref \<lbrace>\<lambda>x y. y = transform s \<and> x = transform_object (machine_state s) oref etcb_opt (kernel_object.CNode radix_bits fun)\<rbrace>
 4. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s)) (KHeap_D.get_object oref)
 5. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))
 6. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (6 subgoals):
 1. \<And>fun rv sa s'. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; sa = transform s'; sa = transform s \<and> rv = transform_object (machine_state s) oref etcb_opt (kernel_object.CNode radix_bits fun); s = s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) ((=) sa) ((=) s') (do cnode <- case rv of cdl_object.CNode x \<Rightarrow> return x | _ \<Rightarrow> fail;
doE y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
y <- whenE (radix_bits < cdl_cnode_size_bits cnode) throw;
if radix_bits \<le> cdl_cnode_size_bits cnode then returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), 0) else doE next_cap <- liftE $ KHeap_D.get_cap (oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode)));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl ref) (radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), radix_bits + length guard - (cdl_cnode_size_bits cnode + length guard))
odE
odE
od) (returnOk ((oref, drop (length guard) ref), []))
 2. \<And>fun sa. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; transform s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> KHeap_D.get_object oref \<exists>\<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s)\<rbrace> KHeap_D.get_object oref \<lbrace>\<lambda>x y. y = transform s \<and> x = transform_object (machine_state s) oref etcb_opt (kernel_object.CNode radix_bits fun)\<rbrace>
 4. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s)) (KHeap_D.get_object oref)
 5. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))
 6. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (6 subgoals):
 1. \<And>fun rv s' x2. \<lbrakk>s = s'; cap = cap.CNodeCap oref (Suc x2) guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) (Suc x2); valid_idle s'; x2 + length guard \<le> 31; valid_objs s'; CSpace_A.resolve_address_bits (cap.CNodeCap oref (Suc x2) guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = Suc (x2 + length guard); guard \<le> ref; (of_bl ref >> Suc x2) && mask (length guard) = of_bl guard; (of_bl ref >> Suc x2) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref (Suc x2) guard); length guard \<le> word_bits; kheap s' oref = Some (kernel_object.CNode (Suc x2) fun); well_formed_cnode_n (Suc x2) fun; radix_bits = Suc x2; rv = cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc x2) fun, cdl_cnode_size_bits = Suc x2\<rparr>\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) ((=) (transform s')) ((=) s') (returnOk ((oref, unat (of_bl ref && mask (Suc x2))), 0)) (returnOk ((oref, drop (length guard) ref), []))
 2. \<And>fun sa. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; transform s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> KHeap_D.get_object oref \<exists>\<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s)\<rbrace> KHeap_D.get_object oref \<lbrace>\<lambda>x y. y = transform s \<and> x = transform_object (machine_state s) oref etcb_opt (kernel_object.CNode radix_bits fun)\<rbrace>
 4. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s)) (KHeap_D.get_object oref)
 5. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))
 6. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (6 subgoals):
 1. \<And>fun x2. \<lbrakk>cap = cap.CNodeCap oref (Suc x2) guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) (Suc x2); valid_idle s; x2 + length guard \<le> 31; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref (Suc x2) guard, ref) = (\<lambda>s. ({(Inr ((oref, drop (length guard) ref), []), s)}, False)); length ref = Suc (x2 + length guard); guard \<le> ref; (of_bl ref >> Suc x2) && mask (length guard) = of_bl guard; (of_bl ref >> Suc x2) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref (Suc x2) guard); length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode (Suc x2) fun); well_formed_cnode_n (Suc x2) fun; radix_bits = Suc x2\<rbrakk> \<Longrightarrow> unat (of_bl ref && mask (Suc x2)) = nat (bl_to_bin (drop (length guard) ref))
 2. \<And>fun sa. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; transform s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> KHeap_D.get_object oref \<exists>\<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s)\<rbrace> KHeap_D.get_object oref \<lbrace>\<lambda>x y. y = transform s \<and> x = transform_object (machine_state s) oref etcb_opt (kernel_object.CNode radix_bits fun)\<rbrace>
 4. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s)) (KHeap_D.get_object oref)
 5. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))
 6. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (6 subgoals):
 1. \<And>fun x2. \<lbrakk>cap = cap.CNodeCap oref (Suc x2) guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) (Suc x2); valid_idle s; x2 + length guard \<le> 31; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref (Suc x2) guard, ref) = (\<lambda>s. ({(Inr ((oref, drop (length guard) ref), []), s)}, False)); length ref = Suc (x2 + length guard); guard \<le> ref; (of_bl ref >> Suc x2) && mask (length guard) = of_bl guard; (of_bl ref >> Suc x2) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref (Suc x2) guard); length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode (Suc x2) fun); well_formed_cnode_n (Suc x2) fun; radix_bits = Suc x2\<rbrakk> \<Longrightarrow> nat (uint (of_bl ref && mask (Suc x2))) = nat (bl_to_bin (drop (length guard) ref))
 2. \<And>fun sa. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; transform s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> KHeap_D.get_object oref \<exists>\<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s)\<rbrace> KHeap_D.get_object oref \<lbrace>\<lambda>x y. y = transform s \<and> x = transform_object (machine_state s) oref etcb_opt (kernel_object.CNode radix_bits fun)\<rbrace>
 4. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s)) (KHeap_D.get_object oref)
 5. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))
 6. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (8 subgoals):
 1. \<And>fun x2. \<lbrakk>cap = cap.CNodeCap oref (Suc x2) guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) (Suc x2); valid_idle s; x2 + length guard \<le> 31; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref (Suc x2) guard, ref) = (\<lambda>s. ({(Inr ((oref, drop (length guard) ref), []), s)}, False)); length ref = Suc (x2 + length guard); guard \<le> ref; (of_bl ref >> Suc x2) && mask (length guard) = of_bl guard; (of_bl ref >> Suc x2) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref (Suc x2) guard); length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode (Suc x2) fun); well_formed_cnode_n (Suc x2) fun; radix_bits = Suc x2\<rbrakk> \<Longrightarrow> 0 \<le> uint (of_bl ref && mask (Suc x2))
 2. \<And>fun x2. \<lbrakk>cap = cap.CNodeCap oref (Suc x2) guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) (Suc x2); valid_idle s; x2 + length guard \<le> 31; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref (Suc x2) guard, ref) = (\<lambda>s. ({(Inr ((oref, drop (length guard) ref), []), s)}, False)); length ref = Suc (x2 + length guard); guard \<le> ref; (of_bl ref >> Suc x2) && mask (length guard) = of_bl guard; (of_bl ref >> Suc x2) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref (Suc x2) guard); length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode (Suc x2) fun); well_formed_cnode_n (Suc x2) fun; radix_bits = Suc x2\<rbrakk> \<Longrightarrow> 0 \<le> bl_to_bin (drop (length guard) ref)
 3. \<And>fun x2. \<lbrakk>cap = cap.CNodeCap oref (Suc x2) guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) (Suc x2); valid_idle s; x2 + length guard \<le> 31; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref (Suc x2) guard, ref) = (\<lambda>s. ({(Inr ((oref, drop (length guard) ref), []), s)}, False)); length ref = Suc (x2 + length guard); guard \<le> ref; (of_bl ref >> Suc x2) && mask (length guard) = of_bl guard; (of_bl ref >> Suc x2) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref (Suc x2) guard); length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode (Suc x2) fun); well_formed_cnode_n (Suc x2) fun; radix_bits = Suc x2\<rbrakk> \<Longrightarrow> uint (of_bl ref && mask (Suc x2)) = bl_to_bin (drop (length guard) ref)
 4. \<And>fun sa. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; transform s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> KHeap_D.get_object oref \<exists>\<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s)\<rbrace> KHeap_D.get_object oref \<lbrace>\<lambda>x y. y = transform s \<and> x = transform_object (machine_state s) oref etcb_opt (kernel_object.CNode radix_bits fun)\<rbrace>
 6. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s)) (KHeap_D.get_object oref)
 7. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))
 8. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (6 subgoals):
 1. \<And>fun x2. \<lbrakk>cap = cap.CNodeCap oref (Suc x2) guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) (Suc x2); valid_idle s; x2 + length guard \<le> 31; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref (Suc x2) guard, ref) = (\<lambda>s. ({(Inr ((oref, drop (length guard) ref), []), s)}, False)); length ref = Suc (x2 + length guard); guard \<le> ref; (of_bl ref >> Suc x2) && mask (length guard) = of_bl guard; (of_bl ref >> Suc x2) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref (Suc x2) guard); length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode (Suc x2) fun); well_formed_cnode_n (Suc x2) fun; radix_bits = Suc x2\<rbrakk> \<Longrightarrow> uint (of_bl ref && mask (Suc x2)) = bl_to_bin (drop (length guard) ref)
 2. \<And>fun sa. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; transform s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> KHeap_D.get_object oref \<exists>\<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s)\<rbrace> KHeap_D.get_object oref \<lbrace>\<lambda>x y. y = transform s \<and> x = transform_object (machine_state s) oref etcb_opt (kernel_object.CNode radix_bits fun)\<rbrace>
 4. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s)) (KHeap_D.get_object oref)
 5. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))
 6. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (6 subgoals):
 1. \<And>fun x2. \<lbrakk>cap = cap.CNodeCap oref (Suc x2) guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) (Suc x2); valid_idle s; x2 + length guard \<le> 31; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref (Suc x2) guard, ref) = (\<lambda>s. ({(Inr ((oref, drop (length guard) ref), []), s)}, False)); length ref = Suc (x2 + length guard); guard \<le> ref; (of_bl ref >> Suc x2) && mask (length guard) = of_bl guard; (of_bl ref >> Suc x2) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref (Suc x2) guard); length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode (Suc x2) fun); well_formed_cnode_n (Suc x2) fun; radix_bits = Suc x2\<rbrakk> \<Longrightarrow> bl_to_bin (to_bl (of_bl ref && mask (Suc x2))) = bl_to_bin (drop (length guard) ref)
 2. \<And>fun sa. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; transform s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> KHeap_D.get_object oref \<exists>\<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s)\<rbrace> KHeap_D.get_object oref \<lbrace>\<lambda>x y. y = transform s \<and> x = transform_object (machine_state s) oref etcb_opt (kernel_object.CNode radix_bits fun)\<rbrace>
 4. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s)) (KHeap_D.get_object oref)
 5. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))
 6. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (6 subgoals):
 1. \<And>fun x2. \<lbrakk>cap = cap.CNodeCap oref (Suc x2) guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) (Suc x2); valid_idle s; x2 + length guard \<le> 31; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref (Suc x2) guard, ref) = (\<lambda>s. ({(Inr ((oref, drop (length guard) ref), []), s)}, False)); length ref = Suc (x2 + length guard); guard \<le> ref; (of_bl ref >> Suc x2) && mask (length guard) = of_bl guard; (of_bl ref >> Suc x2) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref (Suc x2) guard); length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode (Suc x2) fun); well_formed_cnode_n (Suc x2) fun; radix_bits = Suc x2\<rbrakk> \<Longrightarrow> bl_to_bin (replicate (LENGTH(32) - Suc x2) False @ drop (LENGTH(32) - Suc x2) (to_bl (of_bl ref))) = bl_to_bin (drop (length guard) ref)
 2. \<And>fun sa. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; transform s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> KHeap_D.get_object oref \<exists>\<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s)\<rbrace> KHeap_D.get_object oref \<lbrace>\<lambda>x y. y = transform s \<and> x = transform_object (machine_state s) oref etcb_opt (kernel_object.CNode radix_bits fun)\<rbrace>
 4. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s)) (KHeap_D.get_object oref)
 5. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))
 6. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (5 subgoals):
 1. \<And>fun sa. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; transform s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> KHeap_D.get_object oref \<exists>\<lbrace>\<lambda>r. (=) sa\<rbrace>
 2. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s)\<rbrace> KHeap_D.get_object oref \<lbrace>\<lambda>x y. y = transform s \<and> x = transform_object (machine_state s) oref etcb_opt (kernel_object.CNode radix_bits fun)\<rbrace>
 3. \<And>fun. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard; cap_aligned (cap.CNodeCap oref radix_bits guard); 0 < radix_bits; length guard \<le> word_bits; kheap s oref = Some (kernel_object.CNode radix_bits fun); well_formed_cnode_n radix_bits fun; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s)) (KHeap_D.get_object oref)
 4. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))
 5. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) \<noteq> of_bl guard \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) (\<lambda>_. True) ((=) s) (doE cnode <- liftE (get_cnode oref);
y <- if 0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> [] then returnOk () else fail;
throw
odE) (returnOk ((oref, drop (length guard) ref), []))
 2. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref\<rbrakk> \<Longrightarrow> to_bl (of_bl ref) = ?xs297 @ ref
 2. \<lbrakk>cap = cap.CNodeCap oref radix_bits guard; cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; radix_bits + length guard \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = returnOk ((oref, drop (length guard) ref), []); 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard; guard \<le> ref; length guard \<le> length ref \<and> (of_bl ref >> length ref - length guard) && mask (length guard) = of_bl guard\<rbrakk> \<Longrightarrow> (of_bl ref >> radix_bits) && mask (length guard) = of_bl guard proof (prove)
goal:
No subgoals!