theory KHeap_DR

lemma resolve_address_bits_error_corres:
  "\<lbrakk> cap'= transform_cap cap;
     0<radix_bits \<or> guard \<noteq> [];
     \<not>in_terminate_branch ref cap;
     \<not> in_recursive_branch ref cap;
     cap = cap.CNodeCap oref radix_bits guard;
     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) apply (frule resolve_address_bits_error_branch2[where 'a=det_ext]) apply simp+ apply (clarsimp) apply (simp add:transform_cap_def cap_type_simps unlessE_def) apply (clarsimp simp: in_terminate_branch_def in_recursive_branch_def | rule conjI)+ apply (clarsimp simp: assertE_def 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 (clarsimp simp:whenE_def branch_map_simp1 split: nat.splits|rule conjI)+ apply (drule (1) transform_objects_cnode, simp,
            clarsimp simp:transform_objects_cnode gets_the_def gets_def get_def
                          bind_def return_def valid_def exs_valid_def
                          assert_opt_def transform_def
                     split: nat.splits)+ 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 (rule dcorres_expand_pfx) apply clarsimp apply (rename_tac "fun") 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 (clarsimp simp:whenE_def branch_map_simp1|rule conjI)+ apply (drule (1) transform_objects_cnode, simp,
            clarsimp simp: transform_objects_cnode gets_the_def gets_def get_def
                           bind_def return_def valid_def exs_valid_def
                           assert_opt_def transform_def
                     split: nat.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap' = transform_cap cap; 0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; 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>cap' = transform_cap cap; 0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; 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) (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 (4 subgoals):
 1. \<lbrakk>cap' = transform_cap cap; 0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap; valid_idle s; length ref \<le> 32; valid_objs s\<rbrakk> \<Longrightarrow> \<not> in_terminate_branch ?ref ?cap
 2. \<lbrakk>cap' = transform_cap cap; 0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap; valid_idle s; length ref \<le> 32; valid_objs s\<rbrakk> \<Longrightarrow> \<not> in_recursive_branch ?ref ?cap
 3. \<lbrakk>cap' = transform_cap cap; 0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap; valid_idle s; length ref \<le> 32; valid_objs s\<rbrakk> \<Longrightarrow> ?cap = cap.CNodeCap ?oref radix_bits guard
 4. \<lbrakk>cap' = transform_cap cap; 0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap; valid_idle s; length ref \<le> 32; valid_objs s; \<exists>excep. CSpace_A.resolve_address_bits (?cap, ?ref) = throwError excep\<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' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; 0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref (cap.CNodeCap oref radix_bits guard); \<not> in_recursive_branch ref (cap.CNodeCap oref radix_bits guard); cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; \<exists>excep. CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep\<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 (length guard \<le> length ref \<and> (of_bl ref >> length ref - length guard) && mask (length guard) = of_bl guard) throw;
y <- whenE (length ref < cdl_cnode_size_bits cnode + length guard) throw;
if length ref \<le> cdl_cnode_size_bits cnode + length guard then returnOk ((oref, unat ((of_bl ref >> length ref - (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 >> length ref - (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) (length ref - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> length ref - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), length ref - (cdl_cnode_size_bits cnode + length guard))
odE
odE) (CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref)) proof (prove)
goal (1 subgoal):
 1. \<And>excep. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; 0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref (cap.CNodeCap oref radix_bits guard); \<not> in_recursive_branch ref (cap.CNodeCap oref radix_bits guard); cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep\<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 (length guard \<le> length ref \<and> (of_bl ref >> length ref - length guard) && mask (length guard) = of_bl guard) throw;
y <- whenE (length ref < cdl_cnode_size_bits cnode + length guard) throw;
if length ref \<le> cdl_cnode_size_bits cnode + length guard then returnOk ((oref, unat ((of_bl ref >> length ref - (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 >> length ref - (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) (length ref - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> length ref - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), length ref - (cdl_cnode_size_bits cnode + length guard))
odE
odE) (throwError excep) proof (prove)
goal (1 subgoal):
 1. \<And>excep. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; 0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref (cap.CNodeCap oref radix_bits guard); \<not> in_recursive_branch ref (cap.CNodeCap oref radix_bits guard); cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep\<rbrakk> \<Longrightarrow> (length guard \<le> length ref \<and> (of_bl ref >> length ref - length guard) && 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
y <- whenE (length ref < cdl_cnode_size_bits cnode + length guard) throw;
if length ref \<le> cdl_cnode_size_bits cnode + length guard then returnOk ((oref, unat ((of_bl ref >> length ref - (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 >> length ref - (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) (length ref - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> length ref - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), length ref - (cdl_cnode_size_bits cnode + length guard))
odE
odE) (throwError excep)) \<and> ((length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE) (throwError excep)) proof (prove)
goal (2 subgoals):
 1. \<And>excep. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref; (of_bl ref >> length ref - length guard) && 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
y <- whenE (length ref < cdl_cnode_size_bits cnode + length guard) throw;
if length ref \<le> cdl_cnode_size_bits cnode + length guard then returnOk ((oref, unat ((of_bl ref >> length ref - (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 >> length ref - (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) (length ref - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> length ref - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), length ref - (cdl_cnode_size_bits cnode + length guard))
odE
odE) (throwError excep)
 2. \<And>excep. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep\<rbrakk> \<Longrightarrow> (length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE) (throwError excep) proof (prove)
goal (2 subgoals):
 1. \<And>excep. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref; (of_bl ref >> length ref - length guard) && 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 (length ref < cdl_cnode_size_bits cnode + length guard) throw;
if length ref \<le> cdl_cnode_size_bits cnode + length guard then returnOk ((oref, unat ((of_bl ref >> length ref - (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 >> length ref - (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) (length ref - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> length ref - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), length ref - (cdl_cnode_size_bits cnode + length guard))
odE
odE
od) (throwError excep)
 2. \<And>excep. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep\<rbrakk> \<Longrightarrow> (length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE) (throwError excep) proof (prove)
goal (2 subgoals):
 1. \<And>excep ko. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref; (of_bl ref >> length ref - length guard) && 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 (length ref < cdl_cnode_size_bits cnode + length guard) throw;
if length ref \<le> cdl_cnode_size_bits cnode + length guard then returnOk ((oref, unat ((of_bl ref >> length ref - (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 >> length ref - (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) (length ref - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> length ref - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), length ref - (cdl_cnode_size_bits cnode + length guard))
odE
odE
od) (throwError excep)
 2. \<And>excep. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep\<rbrakk> \<Longrightarrow> (length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE) (throwError excep) proof (prove)
goal (2 subgoals):
 1. \<And>excep x12. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref; (of_bl ref >> length ref - length guard) && 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 (length ref < cdl_cnode_size_bits cnode + length guard) throw;
if length ref \<le> cdl_cnode_size_bits cnode + length guard then returnOk ((oref, unat ((of_bl ref >> length ref - (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 >> length ref - (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) (length ref - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> length ref - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), length ref - (cdl_cnode_size_bits cnode + length guard))
odE
odE
od) (throwError excep)
 2. \<And>excep. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep\<rbrakk> \<Longrightarrow> (length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE) (throwError excep) proof (prove)
goal (2 subgoals):
 1. \<And>excep fun. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref; (of_bl ref >> length ref - length guard) && 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 (length ref < cdl_cnode_size_bits cnode + length guard) throw;
if length ref \<le> cdl_cnode_size_bits cnode + length guard then returnOk ((oref, unat ((of_bl ref >> length ref - (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 >> length ref - (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) (length ref - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> length ref - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), length ref - (cdl_cnode_size_bits cnode + length guard))
odE
odE
od) (throwError excep)
 2. \<And>excep. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep\<rbrakk> \<Longrightarrow> (length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE) (throwError excep) proof (prove)
goal (2 subgoals):
 1. \<And>excep fun sa s'. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref; (of_bl ref >> length ref - length guard) && 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 (length ref < cdl_cnode_size_bits cnode + length guard) throw;
if length ref \<le> cdl_cnode_size_bits cnode + length guard then returnOk ((oref, unat ((of_bl ref >> length ref - (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 >> length ref - (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) (length ref - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> length ref - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), length ref - (cdl_cnode_size_bits cnode + length guard))
odE
odE
od) (throwError excep)
 2. \<And>excep. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep\<rbrakk> \<Longrightarrow> (length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE) (throwError excep) proof (prove)
goal (2 subgoals):
 1. \<And>excep fun. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref; (of_bl ref >> length ref - length guard) && 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 (length ref < cdl_cnode_size_bits cnode + length guard) throw;
if length ref \<le> cdl_cnode_size_bits cnode + length guard then returnOk ((oref, unat ((of_bl ref >> length ref - (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 >> length ref - (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) (length ref - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> length ref - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), length ref - (cdl_cnode_size_bits cnode + length guard))
odE
odE
od) (throwError excep)
 2. \<And>excep. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep\<rbrakk> \<Longrightarrow> (length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE) (throwError excep) proof (prove)
goal (5 subgoals):
 1. \<And>excep fun rv. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref; (of_bl ref >> length ref - length guard) && 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 (length ref < cdl_cnode_size_bits cnode + length guard) throw;
if length ref \<le> cdl_cnode_size_bits cnode + length guard then returnOk ((oref, unat ((of_bl ref >> length ref - (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 >> length ref - (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) (length ref - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> length ref - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), length ref - (cdl_cnode_size_bits cnode + length guard))
odE
odE
od) (throwError excep)
 2. \<And>excep fun sa. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref; (of_bl ref >> length ref - length guard) && 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>excep fun. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref; (of_bl ref >> length ref - length guard) && 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>excep fun. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref; (of_bl ref >> length ref - length guard) && 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. \<And>excep. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep\<rbrakk> \<Longrightarrow> (length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE) (throwError excep) proof (prove)
goal (5 subgoals):
 1. \<And>excep fun rv sa s'. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref; (of_bl ref >> length ref - length guard) && 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 (length ref < cdl_cnode_size_bits cnode + length guard) throw;
if length ref \<le> cdl_cnode_size_bits cnode + length guard then returnOk ((oref, unat ((of_bl ref >> length ref - (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 >> length ref - (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) (length ref - (cdl_cnode_size_bits cnode + length guard)) else returnOk ((oref, unat ((of_bl ref >> length ref - (cdl_cnode_size_bits cnode + length guard)) && mask (cdl_cnode_size_bits cnode))), length ref - (cdl_cnode_size_bits cnode + length guard))
odE
odE
od) (throwError excep)
 2. \<And>excep fun sa. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref; (of_bl ref >> length ref - length guard) && 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>excep fun. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref; (of_bl ref >> length ref - length guard) && 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>excep fun. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref; (of_bl ref >> length ref - length guard) && 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. \<And>excep. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep\<rbrakk> \<Longrightarrow> (length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE) (throwError excep) proof (prove)
goal (4 subgoals):
 1. \<And>excep fun. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref \<noteq> radix_bits + length guard; \<not> radix_bits + length guard < length ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref; guard \<le> ref; cap_aligned (cap.CNodeCap oref radix_bits guard); 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 \<exists>\<lbrace>\<lambda>r. (=) (transform s)\<rbrace>
 2. \<And>excep fun. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref; (of_bl ref >> length ref - length guard) && 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>excep fun. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref; (of_bl ref >> length ref - length guard) && 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. \<And>excep. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep\<rbrakk> \<Longrightarrow> (length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE) (throwError excep) proof (prove)
goal (1 subgoal):
 1. \<And>excep. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep\<rbrakk> \<Longrightarrow> (length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE) (throwError excep) proof (prove)
goal (1 subgoal):
 1. \<And>excep. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; 0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; s \<turnstile> cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && mask (length guard) \<noteq> 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE
od) (throwError excep) proof (prove)
goal (1 subgoal):
 1. \<And>excep ko. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && mask (length guard) \<noteq> 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE
od) (throwError excep) proof (prove)
goal (1 subgoal):
 1. \<And>excep x12. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && mask (length guard) \<noteq> 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE
od) (throwError excep) proof (prove)
goal (1 subgoal):
 1. \<And>excep x12 sa s'. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && mask (length guard) \<noteq> 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; 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE
od) (throwError excep) proof (prove)
goal (1 subgoal):
 1. \<And>excep x12. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && mask (length guard) \<noteq> 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'))) ((=) (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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE
od) (throwError excep) proof (prove)
goal (1 subgoal):
 1. \<And>excep fun. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && mask (length guard) \<noteq> 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE
od) (throwError excep) proof (prove)
goal (4 subgoals):
 1. \<And>excep fun rv. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && mask (length guard) \<noteq> 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE
od) (throwError excep)
 2. \<And>excep fun sa. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && mask (length guard) \<noteq> 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>excep fun. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && mask (length guard) \<noteq> 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>excep fun. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && mask (length guard) \<noteq> 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) proof (prove)
goal (4 subgoals):
 1. \<And>excep fun rv sa s'. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && mask (length guard) \<noteq> 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 <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE
od) (throwError excep)
 2. \<And>excep fun sa. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && mask (length guard) \<noteq> 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>excep fun. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && mask (length guard) \<noteq> 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>excep fun. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && mask (length guard) \<noteq> 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) proof (prove)
goal (4 subgoals):
 1. \<And>excep fun. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref \<longrightarrow> \<not> guard \<le> ref; 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 cnode <- case case radix_bits of 0 \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 fun\<rparr> | Suc nat \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) fun, cdl_cnode_size_bits = Suc nat\<rparr> of cdl_object.CNode x \<Rightarrow> return x | _ \<Rightarrow> fail;
doE y <- assertE (0 < cdl_cnode_size_bits cnode \<or> guard \<noteq> []);
throw
odE
od) (throwError excep)
 2. \<And>excep fun sa. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && mask (length guard) \<noteq> 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>excep fun. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && mask (length guard) \<noteq> 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>excep fun. \<lbrakk>cap' = cdl_cap.CNodeCap oref (of_bl guard) (length guard) radix_bits; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; valid_idle s; length ref \<le> 32; valid_objs s; CSpace_A.resolve_address_bits (cap.CNodeCap oref radix_bits guard, ref) = throwError excep; length guard \<le> length ref \<longrightarrow> (of_bl ref >> length ref - length guard) && mask (length guard) \<noteq> 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) proof (prove)
goal:
No subgoals!