theory KHeap_DR

lemma resolve_address_bits_corres':
shows "\<lbrakk>length cref \<le> n ; length cref \<le> 32; cap = transform_cap cap'; wlen = length cref\<rbrakk> \<Longrightarrow>
  dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y)))
   \<top>
   (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs)
  (CSpace_D.resolve_address_bits cap (of_bl cref) wlen)
  (CSpace_A.resolve_address_bits (cap', cref) :: ((cslot_ptr * cap_ref),det_ext) lf_monad)" apply (subgoal_tac "length cref \<le> n \<and> (length cref \<le> 32) \<and> cap = transform_cap cap' \<longrightarrow>
    dcorres (dc\<oplus>(\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y)))
    \<top> (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs)
    (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (resolve_address_bits (cap', cref) :: ((cslot_ptr * cap_ref),det_ext) lf_monad)") apply clarsimp apply (thin_tac "P" for P)+ proof (induct n arbitrary: cref cap' cap) case 0 show ?case apply clarify apply (case_tac "\<not> is_cnode_cap cap'") apply (subst cdl_resolve_address_bits_error_branch1,simp) apply (subst resolve_address_bits_error_branch1,simp) apply simp apply (rule dcorres_expand_pfx) apply (clarsimp simp:gets_the_def gets_def valid_cap_def obj_at_def split:Structures_A.kernel_object.splits cap.splits) apply (clarsimp simp:dc_def[symmetric] is_cap_table_def split:Structures_A.kernel_object.splits cap.splits) apply (rename_tac word nat list "fun") apply (rule corres_guard_imp) apply (rule_tac radix_bits = nat and guard = list and s = s' in resolve_address_bits_error_corres[where ref="[]",simplified]) apply ((simp add:transform_cap_def in_terminate_branch_def in_recursive_branch_def valid_cap_def obj_at_def is_cap_table_def)+)[10] done next case (Suc m) show ?case supply if_cong[cong] apply clarify apply (case_tac "\<not> is_cnode_cap cap'") apply (subst cdl_resolve_address_bits_error_branch1,simp) apply (subst resolve_address_bits_error_branch1,simp) apply simp apply (clarsimp simp:dc_def[symmetric]) apply (rule dcorres_expand_pfx) apply (case_tac "in_terminate_branch cref cap'") apply (clarsimp simp:gets_the_def gets_def valid_cap_def obj_at_def split:Structures_A.kernel_object.splits cap.splits) apply (clarsimp simp:dc_def[symmetric] is_cap_table_def split:Structures_A.kernel_object.splits cap.splits) apply (rule corres_guard_imp) apply (rule_tac s=s' in resolve_address_bits_terminate_corres) apply (simp_all |rule conjI)+ apply (clarsimp simp:valid_cap_def obj_at_def is_cap_table_def) apply (case_tac "\<not> in_recursive_branch cref cap'") apply (clarsimp simp:gets_the_def gets_def valid_cap_def obj_at_def split:Structures_A.kernel_object.splits cap.splits) apply (clarsimp simp:dc_def[symmetric] is_cap_table_def split:Structures_A.kernel_object.splits cap.splits) apply (rename_tac word nat list "fun") apply (rule corres_guard_imp) apply (rule_tac s=s' and radix_bits = nat and guard = list in resolve_address_bits_error_corres) apply (simp_all | rule conjI)+ apply (clarsimp simp:valid_cap_def obj_at_def is_cap_table_def) apply (clarsimp simp:gets_the_def gets_def valid_cap_def obj_at_def split:Structures_A.kernel_object.splits cap.splits) apply (clarsimp simp:dc_def[symmetric] is_cap_table_def split:Structures_A.kernel_object.splits cap.splits) apply (subst KHeap_DR.resolve_address_bits.simps,subst resolve_address_bits_recursive_branch) apply (clarsimp simp:cap_type_simps is_cap_simps)+ apply fastforce apply (rename_tac word nat list "fun") apply (simp add:cap_type_simps) apply (simp add:in_recursive_branch_def in_terminate_branch_def unlessE_def branch_map_simp1) apply (clarsimp simp:get_cnode_def bind_assoc liftE_bindE) apply (rule dcorres_expand_pfx) apply clarsimp apply (rule_tac Q="\<lambda>x y. y = (transform s'a) \<and> x = (transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun))" in corres_symb_exec_l) apply (rule dcorres_expand_pfx) apply (clarsimp simp: nat_case_split) apply (rule corres_split_forwards' [where
                 Q = "\<lambda>rv s. True" and
                 Q' = "\<lambda>next_cap. valid_objs and (\<lambda>a. a \<turnstile> next_cap) and valid_global_refs and
                                  valid_idle and valid_etcbs"]) apply (rule get_cap_corres[THEN corres_guard_imp]) apply (clarsimp simp:transform_cslot_ptr_def) apply (simp add: branch_map_simp2) apply clarsimp apply clarsimp apply (erule (1) cnode_not_idle) apply (wp |simp)+ apply (clarsimp simp:cdl_resolve_address_bits_eq is_cnode_cap_transform_cap | rule conjI)+ apply (subst cdl_resolve_address_bits_eq) apply (subgoal_tac "a+b-a \<le> b" for a b) apply simp+ apply (subst length_drop) apply (rule Suc.hyps[rule_format]) apply fastforce apply (clarsimp simp:returnOk_def transform_cslot_ptr_def) apply (simp add: branch_map_simp2) 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 nat_case_split)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length cref \<le> n; length cref \<le> 32; cap = transform_cap cap'; wlen = length cref\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) wlen) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length cref \<le> n; length cref \<le> 32; cap = transform_cap cap'; wlen = length cref; length cref \<le> n \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) wlen) (CSpace_A.resolve_address_bits (cap', cref))
 2. \<lbrakk>length cref \<le> n; length cref \<le> 32; cap = transform_cap cap'; wlen = length cref\<rbrakk> \<Longrightarrow> length cref \<le> n \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length cref \<le> n; length cref \<le> 32; cap = transform_cap cap'; wlen = length cref\<rbrakk> \<Longrightarrow> length cref \<le> n \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (1 subgoal):
 1. length cref \<le> n \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (state)
goal (2 subgoals):
 1. \<And>cref cap' cap. length cref \<le> 0 \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref))
 2. \<And>n cref cap' cap. (\<And>cref cap' cap. length cref \<le> n \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref))) \<Longrightarrow> length cref \<le> Suc n \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (state)
this:


goal (2 subgoals):
 1. \<And>cref cap' cap. length cref \<le> 0 \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref))
 2. \<And>n cref cap' cap. (\<And>cref cap' cap. length cref \<le> n \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref))) \<Longrightarrow> length cref \<le> Suc n \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (1 subgoal):
 1. length cref \<le> 0 \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and (\<lambda>a. a \<turnstile> cap') and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cref = []; length [] \<le> 32; cap = transform_cap cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and (\<lambda>a. a \<turnstile> cap') and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl []) (length [])) (CSpace_A.resolve_address_bits (cap', [])) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cref = []; length [] \<le> 32; cap = transform_cap cap'; \<not> Structures_A.is_cnode_cap cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and (\<lambda>a. a \<turnstile> cap') and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl []) (length [])) (CSpace_A.resolve_address_bits (cap', []))
 2. \<lbrakk>cref = []; length [] \<le> 32; cap = transform_cap cap'; \<not> \<not> Structures_A.is_cnode_cap cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and (\<lambda>a. a \<turnstile> cap') and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl []) (length [])) (CSpace_A.resolve_address_bits (cap', [])) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cref = []; length [] \<le> 32; cap = transform_cap cap'; \<not> Structures_A.is_cnode_cap cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) throw (CSpace_A.resolve_address_bits (cap', []))
 2. \<lbrakk>cref = []; length [] \<le> 32; cap = transform_cap cap'; \<not> \<not> Structures_A.is_cnode_cap cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and (\<lambda>a. a \<turnstile> cap') and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl []) (length [])) (CSpace_A.resolve_address_bits (cap', [])) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cref = []; length [] \<le> 32; cap = transform_cap cap'; \<not> Structures_A.is_cnode_cap cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) throw (throwError InvalidRoot)
 2. \<lbrakk>cref = []; length [] \<le> 32; cap = transform_cap cap'; \<not> \<not> Structures_A.is_cnode_cap cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and (\<lambda>a. a \<turnstile> cap') and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl []) (length [])) (CSpace_A.resolve_address_bits (cap', [])) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cref = []; length [] \<le> 32; cap = transform_cap cap'; \<not> \<not> Structures_A.is_cnode_cap cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and (\<lambda>a. a \<turnstile> cap') and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl []) (length [])) (CSpace_A.resolve_address_bits (cap', [])) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>cref = []; length [] \<le> 32; cap = transform_cap cap'; \<not> \<not> Structures_A.is_cnode_cap cap'; s = transform s'; True; (valid_objs and (\<lambda>a. a \<turnstile> cap') and valid_global_refs and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) s) ((=) s') (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl []) (length [])) (CSpace_A.resolve_address_bits (cap', [])) proof (prove)
goal (1 subgoal):
 1. \<And>s' x61 x62 x63 ko. \<lbrakk>cref = []; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some ko; is_cap_table x62 ko; length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres ((\<lambda>a b. True) \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62) 0 0) (CSpace_A.resolve_address_bits (cap.CNodeCap x61 x62 x63, [])) proof (prove)
goal (1 subgoal):
 1. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; cref = []; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62) 0 0) (CSpace_A.resolve_address_bits (cap.CNodeCap x61 x62 x63, [])) proof (prove)
goal (1 subgoal):
 1. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; cref = []; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (cdl_cap.CNodeCap word (of_bl list) (length list) nat) 0 0) (CSpace_A.resolve_address_bits (cap.CNodeCap word nat list, [])) proof (prove)
goal (3 subgoals):
 1. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; cref = []; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (?Q116 s' word nat list fun) (?Q'116 s' word nat list fun) (CSpace_D.resolve_address_bits (cdl_cap.CNodeCap word (of_bl list) (length list) nat) 0 0) (CSpace_A.resolve_address_bits (cap.CNodeCap word nat list, []))
 2. \<And>s' word nat list fun s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; cref = []; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; transform s' = s\<rbrakk> \<Longrightarrow> ?Q116 s' word nat list fun s
 3. \<And>s' word nat list fun s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; cref = []; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; s' = s\<rbrakk> \<Longrightarrow> ?Q'116 s' word nat list fun s proof (prove)
goal (10 subgoals):
 1. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; cref = []; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> cdl_cap.CNodeCap word (of_bl list) (length list) nat = transform_cap (cap.CNodeCap word nat list)
 2. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; cref = []; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> 0 < nat \<or> list \<noteq> []
 3. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; cref = []; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> \<not> in_terminate_branch [] (cap.CNodeCap word nat list)
 4. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; cref = []; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> \<not> in_recursive_branch [] (cap.CNodeCap word nat list)
 5. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; cref = []; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> cap.CNodeCap word nat list = cap.CNodeCap (?oref120 s' word nat list fun) nat list
 6. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; cref = []; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> s' \<turnstile> cap.CNodeCap word nat list
 7. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; cref = []; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> valid_idle s'
 8. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; cref = []; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> valid_objs s'
 9. \<And>s' word nat list fun s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; cref = []; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; transform s' = s\<rbrakk> \<Longrightarrow> True
 10. \<And>s' word nat list fun s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; cref = []; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; s' = s\<rbrakk> \<Longrightarrow> s' = s proof (prove)
goal:
No subgoals! proof (state)
this:
length cref \<le> 0 \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and (\<lambda>a. a \<turnstile> cap') and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref))

goal (1 subgoal):
 1. \<And>n cref cap' cap. (\<And>cref cap' cap. length cref \<le> n \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref))) \<Longrightarrow> length cref \<le> Suc n \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (state)
goal (1 subgoal):
 1. \<And>n cref cap' cap. (\<And>cref cap' cap. length cref \<le> n \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref))) \<Longrightarrow> length cref \<le> Suc n \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (state)
this:
length ?cref \<le> m \<and> length ?cref \<le> 32 \<and> ?cap = transform_cap ?cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and (\<lambda>a. a \<turnstile> ?cap') and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits ?cap (of_bl ?cref) (length ?cref)) (CSpace_A.resolve_address_bits (?cap', ?cref))

goal (1 subgoal):
 1. \<And>n cref cap' cap. (\<And>cref cap' cap. length cref \<le> n \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref))) \<Longrightarrow> length cref \<le> Suc n \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (1 subgoal):
 1. length cref \<le> Suc m \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and (\<lambda>a. a \<turnstile> cap') and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (1 subgoal):
 1. length cref \<le> Suc m \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and (\<lambda>a. a \<turnstile> cap') and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and (\<lambda>a. a \<turnstile> cap') and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; \<not> Structures_A.is_cnode_cap cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and (\<lambda>a. a \<turnstile> cap') and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref))
 2. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; \<not> \<not> Structures_A.is_cnode_cap cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and (\<lambda>a. a \<turnstile> cap') and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; \<not> Structures_A.is_cnode_cap cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) throw (CSpace_A.resolve_address_bits (cap', cref))
 2. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; \<not> \<not> Structures_A.is_cnode_cap cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and (\<lambda>a. a \<turnstile> cap') and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; \<not> Structures_A.is_cnode_cap cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs) throw (throwError InvalidRoot)
 2. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; \<not> \<not> Structures_A.is_cnode_cap cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and (\<lambda>a. a \<turnstile> cap') and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; \<not> \<not> Structures_A.is_cnode_cap cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and (\<lambda>a. a \<turnstile> cap') and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; Structures_A.is_cnode_cap cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (\<lambda>a. valid_objs a \<and> a \<turnstile> cap' \<and> valid_global_refs a \<and> valid_idle a \<and> valid_etcbs a) (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; Structures_A.is_cnode_cap cap'; s = transform s'; True; valid_objs s' \<and> s' \<turnstile> cap' \<and> valid_global_refs s' \<and> valid_idle s' \<and> valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) s) ((=) s') (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; Structures_A.is_cnode_cap cap'; s = transform s'; True; valid_objs s' \<and> s' \<turnstile> cap' \<and> valid_global_refs s' \<and> valid_idle s' \<and> valid_etcbs s'; in_terminate_branch cref cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) s) ((=) s') (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref))
 2. \<And>s s'. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; Structures_A.is_cnode_cap cap'; s = transform s'; True; valid_objs s' \<and> s' \<turnstile> cap' \<and> valid_global_refs s' \<and> valid_idle s' \<and> valid_etcbs s'; \<not> in_terminate_branch cref cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) s) ((=) s') (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (2 subgoals):
 1. \<And>s' x61 x62 x63 ko. \<lbrakk>in_terminate_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some ko; is_cap_table x62 ko; length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62) (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap.CNodeCap x61 x62 x63, cref))
 2. \<And>s s'. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; Structures_A.is_cnode_cap cap'; s = transform s'; True; valid_objs s' \<and> s' \<turnstile> cap' \<and> valid_global_refs s' \<and> valid_idle s' \<and> valid_etcbs s'; \<not> in_terminate_branch cref cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) s) ((=) s') (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (2 subgoals):
 1. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; in_terminate_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62) (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap.CNodeCap x61 x62 x63, cref))
 2. \<And>s s'. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; Structures_A.is_cnode_cap cap'; s = transform s'; True; valid_objs s' \<and> s' \<turnstile> cap' \<and> valid_global_refs s' \<and> valid_idle s' \<and> valid_etcbs s'; \<not> in_terminate_branch cref cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) s) ((=) s') (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (4 subgoals):
 1. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; in_terminate_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (?Q117 s' x61 x62 x63 x12) (?Q'117 s' x61 x62 x63 x12) (CSpace_D.resolve_address_bits (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62) (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap.CNodeCap x61 x62 x63, cref))
 2. \<And>s' x61 x62 x63 x12 s. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; in_terminate_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12; transform s' = s\<rbrakk> \<Longrightarrow> ?Q117 s' x61 x62 x63 x12 s
 3. \<And>s' x61 x62 x63 x12 s. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; in_terminate_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12; s' = s\<rbrakk> \<Longrightarrow> ?Q'117 s' x61 x62 x63 x12 s
 4. \<And>s s'. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; Structures_A.is_cnode_cap cap'; s = transform s'; True; valid_objs s' \<and> s' \<turnstile> cap' \<and> valid_global_refs s' \<and> valid_idle s' \<and> valid_etcbs s'; \<not> in_terminate_branch cref cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) s) ((=) s') (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (10 subgoals):
 1. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; in_terminate_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> in_terminate_branch cref (cap.CNodeCap x61 x62 x63)
 2. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; in_terminate_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> cap.CNodeCap x61 x62 x63 = cap.CNodeCap (?oref121 s' x61 x62 x63 x12) (?radix_bits121 s' x61 x62 x63 x12) (?guard121 s' x61 x62 x63 x12)
 3. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; in_terminate_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62 = transform_cap (cap.CNodeCap x61 x62 x63)
 4. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; in_terminate_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> s' \<turnstile> cap.CNodeCap x61 x62 x63
 5. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; in_terminate_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> valid_idle s'
 6. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; in_terminate_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> length cref \<le> 32
 7. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; in_terminate_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> valid_objs s'
 8. \<And>s' x61 x62 x63 x12 s. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; in_terminate_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12; transform s' = s\<rbrakk> \<Longrightarrow> True
 9. \<And>s' x61 x62 x63 x12 s. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; in_terminate_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12; s' = s\<rbrakk> \<Longrightarrow> s' = s
 10. \<And>s s'. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; Structures_A.is_cnode_cap cap'; s = transform s'; True; valid_objs s' \<and> s' \<turnstile> cap' \<and> valid_global_refs s' \<and> valid_idle s' \<and> valid_etcbs s'; \<not> in_terminate_branch cref cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) s) ((=) s') (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (2 subgoals):
 1. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; in_terminate_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> s' \<turnstile> cap.CNodeCap x61 x62 x63
 2. \<And>s s'. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; Structures_A.is_cnode_cap cap'; s = transform s'; valid_objs s' \<and> s' \<turnstile> cap' \<and> valid_global_refs s' \<and> valid_idle s' \<and> valid_etcbs s'; \<not> in_terminate_branch cref cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; Structures_A.is_cnode_cap cap'; s = transform s'; valid_objs s' \<and> s' \<turnstile> cap' \<and> valid_global_refs s' \<and> valid_idle s' \<and> valid_etcbs s'; \<not> in_terminate_branch cref cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; Structures_A.is_cnode_cap cap'; s = transform s'; valid_objs s' \<and> s' \<turnstile> cap' \<and> valid_global_refs s' \<and> valid_idle s' \<and> valid_etcbs s'; \<not> in_terminate_branch cref cap'; \<not> in_recursive_branch cref cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref))
 2. \<And>s s'. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; Structures_A.is_cnode_cap cap'; s = transform s'; valid_objs s' \<and> s' \<turnstile> cap' \<and> valid_global_refs s' \<and> valid_idle s' \<and> valid_etcbs s'; \<not> in_terminate_branch cref cap'; \<not> \<not> in_recursive_branch cref cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (2 subgoals):
 1. \<And>s' x61 x62 x63 ko. \<lbrakk>\<not> in_terminate_branch cref (cap.CNodeCap x61 x62 x63); \<not> in_recursive_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some ko; is_cap_table x62 ko; length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62) (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap.CNodeCap x61 x62 x63, cref))
 2. \<And>s s'. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; Structures_A.is_cnode_cap cap'; s = transform s'; valid_objs s' \<and> s' \<turnstile> cap' \<and> valid_global_refs s' \<and> valid_idle s' \<and> valid_etcbs s'; \<not> in_terminate_branch cref cap'; \<not> \<not> in_recursive_branch cref cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (2 subgoals):
 1. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap x61 x62 x63); \<not> in_recursive_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62) (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap.CNodeCap x61 x62 x63, cref))
 2. \<And>s s'. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; Structures_A.is_cnode_cap cap'; s = transform s'; valid_objs s' \<and> s' \<turnstile> cap' \<and> valid_global_refs s' \<and> valid_idle s' \<and> valid_etcbs s'; \<not> in_terminate_branch cref cap'; \<not> \<not> in_recursive_branch cref cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (2 subgoals):
 1. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap word nat list); \<not> in_recursive_branch cref (cap.CNodeCap word nat list); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (cdl_cap.CNodeCap word (of_bl list) (length list) nat) (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap.CNodeCap word nat list, cref))
 2. \<And>s s'. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; Structures_A.is_cnode_cap cap'; s = transform s'; valid_objs s' \<and> s' \<turnstile> cap' \<and> valid_global_refs s' \<and> valid_idle s' \<and> valid_etcbs s'; \<not> in_terminate_branch cref cap'; \<not> \<not> in_recursive_branch cref cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (4 subgoals):
 1. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap word nat list); \<not> in_recursive_branch cref (cap.CNodeCap word nat list); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (?Q232 s' word nat list fun) (?Q'232 s' word nat list fun) (CSpace_D.resolve_address_bits (cdl_cap.CNodeCap word (of_bl list) (length list) nat) (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap.CNodeCap word nat list, cref))
 2. \<And>s' word nat list fun s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap word nat list); \<not> in_recursive_branch cref (cap.CNodeCap word nat list); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; transform s' = s\<rbrakk> \<Longrightarrow> ?Q232 s' word nat list fun s
 3. \<And>s' word nat list fun s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap word nat list); \<not> in_recursive_branch cref (cap.CNodeCap word nat list); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; s' = s\<rbrakk> \<Longrightarrow> ?Q'232 s' word nat list fun s
 4. \<And>s s'. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; Structures_A.is_cnode_cap cap'; s = transform s'; valid_objs s' \<and> s' \<turnstile> cap' \<and> valid_global_refs s' \<and> valid_idle s' \<and> valid_etcbs s'; \<not> in_terminate_branch cref cap'; \<not> \<not> in_recursive_branch cref cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (12 subgoals):
 1. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap word nat list); \<not> in_recursive_branch cref (cap.CNodeCap word nat list); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> cdl_cap.CNodeCap word (of_bl list) (length list) nat = transform_cap (cap.CNodeCap word nat list)
 2. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap word nat list); \<not> in_recursive_branch cref (cap.CNodeCap word nat list); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> 0 < nat \<or> list \<noteq> []
 3. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap word nat list); \<not> in_recursive_branch cref (cap.CNodeCap word nat list); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> \<not> in_terminate_branch cref (cap.CNodeCap word nat list)
 4. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap word nat list); \<not> in_recursive_branch cref (cap.CNodeCap word nat list); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> \<not> in_recursive_branch cref (cap.CNodeCap word nat list)
 5. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap word nat list); \<not> in_recursive_branch cref (cap.CNodeCap word nat list); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> cap.CNodeCap word nat list = cap.CNodeCap (?oref236 s' word nat list fun) nat list
 6. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap word nat list); \<not> in_recursive_branch cref (cap.CNodeCap word nat list); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> s' \<turnstile> cap.CNodeCap word nat list
 7. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap word nat list); \<not> in_recursive_branch cref (cap.CNodeCap word nat list); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> valid_idle s'
 8. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap word nat list); \<not> in_recursive_branch cref (cap.CNodeCap word nat list); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> length cref \<le> 32
 9. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap word nat list); \<not> in_recursive_branch cref (cap.CNodeCap word nat list); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> valid_objs s'
 10. \<And>s' word nat list fun s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap word nat list); \<not> in_recursive_branch cref (cap.CNodeCap word nat list); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; transform s' = s\<rbrakk> \<Longrightarrow> True
A total of 12 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap word nat list); \<not> in_recursive_branch cref (cap.CNodeCap word nat list); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> s' \<turnstile> cap.CNodeCap word nat list
 2. \<And>s s'. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; Structures_A.is_cnode_cap cap'; s = transform s'; valid_objs s' \<and> s' \<turnstile> cap' \<and> valid_global_refs s' \<and> valid_idle s' \<and> valid_etcbs s'; \<not> in_terminate_branch cref cap'; in_recursive_branch cref cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>length cref \<le> Suc m; length cref \<le> 32; cap = transform_cap cap'; Structures_A.is_cnode_cap cap'; s = transform s'; valid_objs s' \<and> s' \<turnstile> cap' \<and> valid_global_refs s' \<and> valid_idle s' \<and> valid_etcbs s'; \<not> in_terminate_branch cref cap'; in_recursive_branch cref cap'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (transform_cap cap') (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref)) proof (prove)
goal (1 subgoal):
 1. \<And>s' x61 x62 x63 ko. \<lbrakk>\<not> in_terminate_branch cref (cap.CNodeCap x61 x62 x63); in_recursive_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some ko; is_cap_table x62 ko; length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62) (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap.CNodeCap x61 x62 x63, cref)) proof (prove)
goal (1 subgoal):
 1. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap x61 x62 x63); in_recursive_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (CSpace_D.resolve_address_bits (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62) (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap.CNodeCap x61 x62 x63, cref)) proof (prove)
goal (3 subgoals):
 1. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap x61 x62 x63); in_recursive_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> in_recursive_branch cref (cap.CNodeCap x61 x62 x63)
 2. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap x61 x62 x63); in_recursive_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> cap.CNodeCap x61 x62 x63 = cap.CNodeCap (?oref339 s' x61 x62 x63 x12) (?radix_bits339 s' x61 x62 x63 x12) (?guard339 s' x61 x62 x63 x12)
 3. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap x61 x62 x63); in_recursive_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (doE unlessE (Types_D.is_cnode_cap (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62)) $ throw;
cnode <- liftE $ get_cnode $ cap_object (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62);
radix_size <- returnOk $ cdl_cnode_size_bits cnode;
guard_size <- returnOk $ cap_guard_size (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62);
cap_guard <- returnOk $ cap_guard (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62);
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl cref >> length cref - guard_size) && mask guard_size;
unlessE (guard_size \<le> length cref \<and> guard = cap_guard) $ throw;
whenE (length cref < level_size) $ throw;
offset <- returnOk $ (of_bl cref >> length cref - level_size) && mask radix_size;
slot <- returnOk (cap_object (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62), unat offset);
size_left <- returnOk (length cref - 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 cref) size_left else returnOk (slot, size_left)
odE
odE) (doE next_cap <- liftE (CSpaceAcc_A.get_cap (?oref339 s' x61 x62 x63 x12, take (?radix_bits339 s' x61 x62 x63 x12) (drop (length (?guard339 s' x61 x62 x63 x12)) cref)));
if Structures_A.is_cnode_cap next_cap then CSpace_A.resolve_address_bits (next_cap, drop (?radix_bits339 s' x61 x62 x63 x12 + length (?guard339 s' x61 x62 x63 x12)) cref) else returnOk ((?oref339 s' x61 x62 x63 x12, take (?radix_bits339 s' x61 x62 x63 x12) (drop (length (?guard339 s' x61 x62 x63 x12)) cref)), drop (?radix_bits339 s' x61 x62 x63 x12 + length (?guard339 s' x61 x62 x63 x12)) cref)
odE) proof (prove)
goal (2 subgoals):
 1. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap x61 x62 x63); in_recursive_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> x61 = ?oref339 s' x61 x62 x63 x12 \<and> x62 = ?radix_bits339 s' x61 x62 x63 x12 \<and> x63 = ?guard339 s' x61 x62 x63 x12
 2. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap x61 x62 x63); in_recursive_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (doE unlessE (Types_D.is_cnode_cap (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62)) $ throw;
cnode <- liftE $ get_cnode $ cap_object (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62);
radix_size <- returnOk $ cdl_cnode_size_bits cnode;
guard_size <- returnOk $ cap_guard_size (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62);
cap_guard <- returnOk $ cap_guard (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62);
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl cref >> length cref - guard_size) && mask guard_size;
unlessE (guard_size \<le> length cref \<and> guard = cap_guard) $ throw;
whenE (length cref < level_size) $ throw;
offset <- returnOk $ (of_bl cref >> length cref - level_size) && mask radix_size;
slot <- returnOk (cap_object (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62), unat offset);
size_left <- returnOk (length cref - 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 cref) size_left else returnOk (slot, size_left)
odE
odE) (doE next_cap <- liftE (CSpaceAcc_A.get_cap (?oref339 s' x61 x62 x63 x12, take (?radix_bits339 s' x61 x62 x63 x12) (drop (length (?guard339 s' x61 x62 x63 x12)) cref)));
if Structures_A.is_cnode_cap next_cap then CSpace_A.resolve_address_bits (next_cap, drop (?radix_bits339 s' x61 x62 x63 x12 + length (?guard339 s' x61 x62 x63 x12)) cref) else returnOk ((?oref339 s' x61 x62 x63 x12, take (?radix_bits339 s' x61 x62 x63 x12) (drop (length (?guard339 s' x61 x62 x63 x12)) cref)), drop (?radix_bits339 s' x61 x62 x63 x12 + length (?guard339 s' x61 x62 x63 x12)) cref)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>s' x61 x62 x63 x12. \<lbrakk>length x63 \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap x61 x62 x63); in_recursive_branch cref (cap.CNodeCap x61 x62 x63); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62; cap' = cap.CNodeCap x61 x62 x63; valid_objs s'; cap_aligned (cap.CNodeCap x61 x62 x63); 0 < x62; kheap s' x61 = Some (kernel_object.CNode x62 x12); well_formed_cnode_n x62 x12\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (doE unlessE (Types_D.is_cnode_cap (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62)) $ throw;
cnode <- liftE $ get_cnode $ cap_object (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62);
radix_size <- returnOk $ cdl_cnode_size_bits cnode;
guard_size <- returnOk $ cap_guard_size (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62);
cap_guard <- returnOk $ cap_guard (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62);
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl cref >> length cref - guard_size) && mask guard_size;
unlessE (guard_size \<le> length cref \<and> guard = cap_guard) $ throw;
whenE (length cref < level_size) $ throw;
offset <- returnOk $ (of_bl cref >> length cref - level_size) && mask radix_size;
slot <- returnOk (cap_object (cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62), unat offset);
size_left <- returnOk (length cref - 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 cref) size_left else returnOk (slot, size_left)
odE
odE) (doE next_cap <- liftE (CSpaceAcc_A.get_cap (x61, take x62 (drop (length x63) cref)));
if Structures_A.is_cnode_cap next_cap then CSpace_A.resolve_address_bits (next_cap, drop (x62 + length x63) cref) else returnOk ((x61, take x62 (drop (length x63) cref)), drop (x62 + length x63) cref)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap word nat list); in_recursive_branch cref (cap.CNodeCap word nat list); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (doE unlessE (Types_D.is_cnode_cap (cdl_cap.CNodeCap word (of_bl list) (length list) nat)) $ throw;
cnode <- liftE $ get_cnode $ cap_object (cdl_cap.CNodeCap word (of_bl list) (length list) nat);
radix_size <- returnOk $ cdl_cnode_size_bits cnode;
guard_size <- returnOk $ cap_guard_size (cdl_cap.CNodeCap word (of_bl list) (length list) nat);
cap_guard <- returnOk $ cap_guard (cdl_cap.CNodeCap word (of_bl list) (length list) nat);
level_size <- returnOk (radix_size + guard_size);
assertE (level_size \<noteq> 0);
guard <- returnOk $ (of_bl cref >> length cref - guard_size) && mask guard_size;
unlessE (guard_size \<le> length cref \<and> guard = cap_guard) $ throw;
whenE (length cref < level_size) $ throw;
offset <- returnOk $ (of_bl cref >> length cref - level_size) && mask radix_size;
slot <- returnOk (cap_object (cdl_cap.CNodeCap word (of_bl list) (length list) nat), unat offset);
size_left <- returnOk (length cref - 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 cref) size_left else returnOk (slot, size_left)
odE
odE) (doE next_cap <- liftE (CSpaceAcc_A.get_cap (word, take nat (drop (length list) cref)));
if Structures_A.is_cnode_cap next_cap then CSpace_A.resolve_address_bits (next_cap, drop (nat + length list) cref) else returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; \<not> in_terminate_branch cref (cap.CNodeCap word nat list); in_recursive_branch cref (cap.CNodeCap word nat list); length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (doE cnode <- liftE (get_cnode word);
y <- assertE (0 < cdl_cnode_size_bits cnode \<or> list \<noteq> []);
y <- unlessE (length list \<le> length cref \<and> (of_bl cref >> length cref - length list) && mask (length list) = of_bl list) throw;
y <- whenE (length cref < cdl_cnode_size_bits cnode + length list) throw;
if length cref \<le> cdl_cnode_size_bits cnode + length list then returnOk ((word, unat (of_bl cref && mask (cdl_cnode_size_bits cnode))), 0) else doE next_cap <- liftE (KHeap_D.get_cap (word, unat ((of_bl cref >> length cref - (cdl_cnode_size_bits cnode + length list)) && mask (cdl_cnode_size_bits cnode))));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) (length cref - (cdl_cnode_size_bits cnode + length list)) else returnOk ((word, unat ((of_bl cref >> length cref - (cdl_cnode_size_bits cnode + length list)) && mask (cdl_cnode_size_bits cnode))), length cref - (cdl_cnode_size_bits cnode + length list))
odE
odE) (doE next_cap <- liftE (CSpaceAcc_A.get_cap (word, take nat (drop (length list) cref)));
if Structures_A.is_cnode_cap next_cap then CSpace_A.resolve_address_bits (next_cap, drop (nat + length list) cref) else returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; nat + length list < length cref \<and> list \<le> cref; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (doE cnode <- liftE (get_cnode word);
y <- assertE (0 < cdl_cnode_size_bits cnode \<or> list \<noteq> []);
y <- whenE (length cref < cdl_cnode_size_bits cnode + length list) throw;
if length cref \<le> cdl_cnode_size_bits cnode + length list then returnOk ((word, unat (of_bl cref && mask (cdl_cnode_size_bits cnode))), 0) else doE next_cap <- liftE (KHeap_D.get_cap (word, unat ((of_bl cref >> length cref - (cdl_cnode_size_bits cnode + length list)) && mask (cdl_cnode_size_bits cnode))));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) (length cref - (cdl_cnode_size_bits cnode + length list)) else returnOk ((word, unat ((of_bl cref >> length cref - (cdl_cnode_size_bits cnode + length list)) && mask (cdl_cnode_size_bits cnode))), length cref - (cdl_cnode_size_bits cnode + length list))
odE
odE) (doE next_cap <- liftE (CSpaceAcc_A.get_cap (word, take nat (drop (length list) cref)));
if Structures_A.is_cnode_cap next_cap then CSpace_A.resolve_address_bits (next_cap, drop (nat + length list) cref) else returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>s' word nat list fun. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (do x <- KHeap_D.get_object word;
cnode <- case x of cdl_object.CNode x \<Rightarrow> return x | _ \<Rightarrow> fail;
doE y <- assertE (0 < cdl_cnode_size_bits cnode \<or> list \<noteq> []);
y <- whenE (length cref < cdl_cnode_size_bits cnode + length list) throw;
if length cref \<le> cdl_cnode_size_bits cnode + length list then returnOk ((word, unat (of_bl cref && mask (cdl_cnode_size_bits cnode))), 0) else do next_cap <- KHeap_D.get_cap (word, unat ((of_bl cref >> length cref - (cdl_cnode_size_bits cnode + length list)) && mask (cdl_cnode_size_bits cnode)));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) (length cref - (cdl_cnode_size_bits cnode + length list)) else returnOk ((word, unat ((of_bl cref >> length cref - (cdl_cnode_size_bits cnode + length list)) && mask (cdl_cnode_size_bits cnode))), length cref - (cdl_cnode_size_bits cnode + length list))
od
odE
od) (do next_cap <- CSpaceAcc_A.get_cap (word, take nat (drop (length list) cref));
if Structures_A.is_cnode_cap next_cap then CSpace_A.resolve_address_bits (next_cap, drop (nat + length list) cref) else returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' word nat list fun s s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; s = transform s'a; transform s' = s; s' = s'a\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) s) ((=) s'a) (do x <- KHeap_D.get_object word;
cnode <- case x of cdl_object.CNode x \<Rightarrow> return x | _ \<Rightarrow> fail;
doE y <- assertE (0 < cdl_cnode_size_bits cnode \<or> list \<noteq> []);
y <- whenE (length cref < cdl_cnode_size_bits cnode + length list) throw;
if length cref \<le> cdl_cnode_size_bits cnode + length list then returnOk ((word, unat (of_bl cref && mask (cdl_cnode_size_bits cnode))), 0) else do next_cap <- KHeap_D.get_cap (word, unat ((of_bl cref >> length cref - (cdl_cnode_size_bits cnode + length list)) && mask (cdl_cnode_size_bits cnode)));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) (length cref - (cdl_cnode_size_bits cnode + length list)) else returnOk ((word, unat ((of_bl cref >> length cref - (cdl_cnode_size_bits cnode + length list)) && mask (cdl_cnode_size_bits cnode))), length cref - (cdl_cnode_size_bits cnode + length list))
od
odE
od) (do next_cap <- CSpaceAcc_A.get_cap (word, take nat (drop (length list) cref));
if Structures_A.is_cnode_cap next_cap then CSpace_A.resolve_address_bits (next_cap, drop (nat + length list) cref) else returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref)
od) proof (prove)
goal (1 subgoal):
 1. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s'a)) ((=) s'a) (do x <- KHeap_D.get_object word;
cnode <- case x of cdl_object.CNode x \<Rightarrow> return x | _ \<Rightarrow> fail;
doE y <- assertE (0 < cdl_cnode_size_bits cnode \<or> list \<noteq> []);
y <- whenE (length cref < cdl_cnode_size_bits cnode + length list) throw;
if length cref \<le> cdl_cnode_size_bits cnode + length list then returnOk ((word, unat (of_bl cref && mask (cdl_cnode_size_bits cnode))), 0) else do next_cap <- KHeap_D.get_cap (word, unat ((of_bl cref >> length cref - (cdl_cnode_size_bits cnode + length list)) && mask (cdl_cnode_size_bits cnode)));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) (length cref - (cdl_cnode_size_bits cnode + length list)) else returnOk ((word, unat ((of_bl cref >> length cref - (cdl_cnode_size_bits cnode + length list)) && mask (cdl_cnode_size_bits cnode))), length cref - (cdl_cnode_size_bits cnode + length list))
od
odE
od) (do next_cap <- CSpaceAcc_A.get_cap (word, take nat (drop (length list) cref));
if Structures_A.is_cnode_cap next_cap then CSpace_A.resolve_address_bits (next_cap, drop (nat + length list) cref) else returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref)
od) proof (prove)
goal (4 subgoals):
 1. \<And>word nat list fun s'a rv. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>y. y = transform s'a \<and> rv = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)) ((=) s'a) (do cnode <- case rv of cdl_object.CNode x \<Rightarrow> return x | _ \<Rightarrow> fail;
doE y <- assertE (0 < cdl_cnode_size_bits cnode \<or> list \<noteq> []);
y <- whenE (length cref < cdl_cnode_size_bits cnode + length list) throw;
if length cref \<le> cdl_cnode_size_bits cnode + length list then returnOk ((word, unat (of_bl cref && mask (cdl_cnode_size_bits cnode))), 0) else do next_cap <- KHeap_D.get_cap (word, unat ((of_bl cref >> length cref - (cdl_cnode_size_bits cnode + length list)) && mask (cdl_cnode_size_bits cnode)));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) (length cref - (cdl_cnode_size_bits cnode + length list)) else returnOk ((word, unat ((of_bl cref >> length cref - (cdl_cnode_size_bits cnode + length list)) && mask (cdl_cnode_size_bits cnode))), length cref - (cdl_cnode_size_bits cnode + length list))
od
odE
od) (do next_cap <- CSpaceAcc_A.get_cap (word, take nat (drop (length list) cref));
if Structures_A.is_cnode_cap next_cap then CSpace_A.resolve_address_bits (next_cap, drop (nat + length list) cref) else returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref)
od)
 2. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 4. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (4 subgoals):
 1. \<And>word nat list fun s'a rv s s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; s = transform s'; s = transform s'a \<and> rv = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun); s'a = s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) s) ((=) 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> list \<noteq> []);
y <- whenE (length cref < cdl_cnode_size_bits cnode + length list) throw;
if length cref \<le> cdl_cnode_size_bits cnode + length list then returnOk ((word, unat (of_bl cref && mask (cdl_cnode_size_bits cnode))), 0) else do next_cap <- KHeap_D.get_cap (word, unat ((of_bl cref >> length cref - (cdl_cnode_size_bits cnode + length list)) && mask (cdl_cnode_size_bits cnode)));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) (length cref - (cdl_cnode_size_bits cnode + length list)) else returnOk ((word, unat ((of_bl cref >> length cref - (cdl_cnode_size_bits cnode + length list)) && mask (cdl_cnode_size_bits cnode))), length cref - (cdl_cnode_size_bits cnode + length list))
od
odE
od) (do next_cap <- CSpaceAcc_A.get_cap (word, take nat (drop (length list) cref));
if Structures_A.is_cnode_cap next_cap then CSpace_A.resolve_address_bits (next_cap, drop (nat + length list) cref) else returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref)
od)
 2. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 4. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (4 subgoals):
 1. \<And>word nat list fun s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) ((=) (transform s')) ((=) s') (do next_cap <- KHeap_D.get_cap (word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat));
if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) (length cref - (nat + length list)) else returnOk ((word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)), length cref - (nat + length list))
od) (do next_cap <- CSpaceAcc_A.get_cap (word, take nat (drop (length list) cref));
if Structures_A.is_cnode_cap next_cap then CSpace_A.resolve_address_bits (next_cap, drop (nat + length list) cref) else returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref)
od)
 2. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 4. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (7 subgoals):
 1. \<And>word nat list fun s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> dcorres (?r'361 word nat list fun s') ((=) (transform s')) ((=) s') (KHeap_D.get_cap (word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat))) (CSpaceAcc_A.get_cap (word, take nat (drop (length list) cref)))
 2. \<And>word nat list fun s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> KHeap_D.get_cap (word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)) \<lbrace>\<lambda>next_cap s. True\<rbrace>
 3. \<And>word nat list fun s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> CSpaceAcc_A.get_cap (word, take nat (drop (length list) cref)) \<lbrace>\<lambda>next_cap. valid_objs and (\<lambda>a. a \<turnstile> next_cap) and valid_global_refs and valid_idle and valid_etcbs\<rbrace>
 4. \<And>word nat list fun s' next_cap next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; ?r'361 word nat list fun s' next_cap next_capa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and (\<lambda>a. a \<turnstile> next_capa) and valid_global_refs and valid_idle and valid_etcbs) (if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) (length cref - (nat + length list)) else returnOk ((word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)), length cref - (nat + length list))) (if Structures_A.is_cnode_cap next_capa then CSpace_A.resolve_address_bits (next_capa, drop (nat + length list) cref) else returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref))
 5. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 7. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (9 subgoals):
 1. \<And>word nat list fun s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> (word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)) = transform_cslot_ptr (word, take nat (drop (length list) cref))
 2. \<And>word nat list fun s' s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s' = s\<rbrakk> \<Longrightarrow> True
 3. \<And>word nat list fun s' s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst (word, take nat (drop (length list) cref))) and valid_etcbs) s
 4. \<And>word nat list fun s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> KHeap_D.get_cap (word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)) \<lbrace>\<lambda>next_cap s. True\<rbrace>
 5. \<And>word nat list fun s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> CSpaceAcc_A.get_cap (word, take nat (drop (length list) cref)) \<lbrace>\<lambda>next_cap. valid_objs and (\<lambda>a. a \<turnstile> next_cap) and valid_global_refs and valid_idle and valid_etcbs\<rbrace>
 6. \<And>word nat list fun s' next_cap next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; next_cap = transform_cap next_capa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and (\<lambda>a. a \<turnstile> next_capa) and valid_global_refs and valid_idle and valid_etcbs) (if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) (length cref - (nat + length list)) else returnOk ((word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)), length cref - (nat + length list))) (if Structures_A.is_cnode_cap next_capa then CSpace_A.resolve_address_bits (next_capa, drop (nat + length list) cref) else returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref))
 7. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 9. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (9 subgoals):
 1. \<And>word nata list fun s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nata; cap' = cap.CNodeCap word nata list; valid_objs s'; cap_aligned (cap.CNodeCap word nata list); 0 < nata; kheap s' word = Some (kernel_object.CNode nata fun); well_formed_cnode_n nata fun; nata + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> unat ((of_bl cref >> length cref - (nata + length list)) && mask nata) = nat (bl_to_bin (take nata (drop (length list) cref)))
 2. \<And>word nat list fun s' s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s' = s\<rbrakk> \<Longrightarrow> True
 3. \<And>word nat list fun s' s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst (word, take nat (drop (length list) cref))) and valid_etcbs) s
 4. \<And>word nat list fun s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> KHeap_D.get_cap (word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)) \<lbrace>\<lambda>next_cap s. True\<rbrace>
 5. \<And>word nat list fun s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> CSpaceAcc_A.get_cap (word, take nat (drop (length list) cref)) \<lbrace>\<lambda>next_cap. valid_objs and (\<lambda>a. a \<turnstile> next_cap) and valid_global_refs and valid_idle and valid_etcbs\<rbrace>
 6. \<And>word nat list fun s' next_cap next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; next_cap = transform_cap next_capa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and (\<lambda>a. a \<turnstile> next_capa) and valid_global_refs and valid_idle and valid_etcbs) (if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) (length cref - (nat + length list)) else returnOk ((word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)), length cref - (nat + length list))) (if Structures_A.is_cnode_cap next_capa then CSpace_A.resolve_address_bits (next_capa, drop (nat + length list) cref) else returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref))
 7. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 9. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (8 subgoals):
 1. \<And>word nat list fun s' s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s' = s\<rbrakk> \<Longrightarrow> True
 2. \<And>word nat list fun s' s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst (word, take nat (drop (length list) cref))) and valid_etcbs) s
 3. \<And>word nat list fun s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> KHeap_D.get_cap (word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)) \<lbrace>\<lambda>next_cap s. True\<rbrace>
 4. \<And>word nat list fun s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> CSpaceAcc_A.get_cap (word, take nat (drop (length list) cref)) \<lbrace>\<lambda>next_cap. valid_objs and (\<lambda>a. a \<turnstile> next_cap) and valid_global_refs and valid_idle and valid_etcbs\<rbrace>
 5. \<And>word nat list fun s' next_cap next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; next_cap = transform_cap next_capa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and (\<lambda>a. a \<turnstile> next_capa) and valid_global_refs and valid_idle and valid_etcbs) (if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) (length cref - (nat + length list)) else returnOk ((word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)), length cref - (nat + length list))) (if Structures_A.is_cnode_cap next_capa then CSpace_A.resolve_address_bits (next_capa, drop (nat + length list) cref) else returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref))
 6. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 8. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (7 subgoals):
 1. \<And>word nat list fun s' s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread (fst (word, take nat (drop (length list) cref))) and valid_etcbs) s
 2. \<And>word nat list fun s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> KHeap_D.get_cap (word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)) \<lbrace>\<lambda>next_cap s. True\<rbrace>
 3. \<And>word nat list fun s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> CSpaceAcc_A.get_cap (word, take nat (drop (length list) cref)) \<lbrace>\<lambda>next_cap. valid_objs and (\<lambda>a. a \<turnstile> next_cap) and valid_global_refs and valid_idle and valid_etcbs\<rbrace>
 4. \<And>word nat list fun s' next_cap next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; next_cap = transform_cap next_capa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and (\<lambda>a. a \<turnstile> next_capa) and valid_global_refs and valid_idle and valid_etcbs) (if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) (length cref - (nat + length list)) else returnOk ((word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)), length cref - (nat + length list))) (if Structures_A.is_cnode_cap next_capa then CSpace_A.resolve_address_bits (next_capa, drop (nat + length list) cref) else returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref))
 5. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 7. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (7 subgoals):
 1. \<And>word nat list fun s. \<lbrakk>length list \<le> word_bits; valid_global_refs s; valid_idle s; valid_etcbs s; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> not_idle_thread word s
 2. \<And>word nat list fun s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> KHeap_D.get_cap (word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)) \<lbrace>\<lambda>next_cap s. True\<rbrace>
 3. \<And>word nat list fun s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> CSpaceAcc_A.get_cap (word, take nat (drop (length list) cref)) \<lbrace>\<lambda>next_cap. valid_objs and (\<lambda>a. a \<turnstile> next_cap) and valid_global_refs and valid_idle and valid_etcbs\<rbrace>
 4. \<And>word nat list fun s' next_cap next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; next_cap = transform_cap next_capa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and (\<lambda>a. a \<turnstile> next_capa) and valid_global_refs and valid_idle and valid_etcbs) (if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) (length cref - (nat + length list)) else returnOk ((word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)), length cref - (nat + length list))) (if Structures_A.is_cnode_cap next_capa then CSpace_A.resolve_address_bits (next_capa, drop (nat + length list) cref) else returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref))
 5. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 7. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (6 subgoals):
 1. \<And>word nat list fun s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> KHeap_D.get_cap (word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)) \<lbrace>\<lambda>next_cap s. True\<rbrace>
 2. \<And>word nat list fun s'. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> CSpaceAcc_A.get_cap (word, take nat (drop (length list) cref)) \<lbrace>\<lambda>next_cap. valid_objs and (\<lambda>a. a \<turnstile> next_cap) and valid_global_refs and valid_idle and valid_etcbs\<rbrace>
 3. \<And>word nat list fun s' next_cap next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; next_cap = transform_cap next_capa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and (\<lambda>a. a \<turnstile> next_capa) and valid_global_refs and valid_idle and valid_etcbs) (if Types_D.is_cnode_cap next_cap then CSpace_D.resolve_address_bits next_cap (of_bl cref) (length cref - (nat + length list)) else returnOk ((word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)), length cref - (nat + length list))) (if Structures_A.is_cnode_cap next_capa then CSpace_A.resolve_address_bits (next_capa, drop (nat + length list) cref) else returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref))
 4. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 6. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (4 subgoals):
 1. \<And>word nat list fun s' next_cap next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; next_cap = transform_cap next_capa\<rbrakk> \<Longrightarrow> (Types_D.is_cnode_cap (transform_cap next_capa) \<longrightarrow> (Structures_A.is_cnode_cap next_capa \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and (\<lambda>a. a \<turnstile> next_capa) and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap next_capa) (of_bl cref) (length cref - (nat + length list))) (CSpace_A.resolve_address_bits (next_capa, drop (nat + length list) cref))) \<and> (\<not> Structures_A.is_cnode_cap next_capa \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and (\<lambda>a. a \<turnstile> next_capa) and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap next_capa) (of_bl cref) (length cref - (nat + length list))) (returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref)))) \<and> (cap_type (transform_cap next_capa) \<noteq> Some CNodeType \<longrightarrow> (Structures_A.is_cnode_cap next_capa \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and (\<lambda>a. a \<turnstile> next_capa) and valid_global_refs and valid_idle and valid_etcbs) (returnOk ((word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)), length cref - (nat + length list))) (CSpace_A.resolve_address_bits (next_capa, drop (nat + length list) cref))) \<and> (\<not> Structures_A.is_cnode_cap next_capa \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and (\<lambda>a. a \<turnstile> next_capa) and valid_global_refs and valid_idle and valid_etcbs) (returnOk ((word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)), length cref - (nat + length list))) (returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref))))
 2. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 4. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (5 subgoals):
 1. \<And>word nat list fun s' next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; Structures_A.is_cnode_cap next_capa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and valid_cap next_capa and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap next_capa) (of_bl cref) (length cref - (nat + length list))) (CSpace_A.resolve_address_bits (next_capa, drop (nat + length list) cref))
 2. \<And>word nat list fun s' next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<not> Structures_A.is_cnode_cap next_capa \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and valid_cap next_capa and valid_global_refs and valid_idle and valid_etcbs) (returnOk ((word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)), length cref - (nat + length list))) (returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref))
 3. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 5. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (6 subgoals):
 1. \<And>word nat list fun s' next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; Structures_A.is_cnode_cap next_capa\<rbrakk> \<Longrightarrow> ?a412 word nat list fun s' next_capa + (length cref - (nat + length list)) \<le> length cref \<and> length cref \<le> 32
 2. \<And>word nat list fun s' next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; Structures_A.is_cnode_cap next_capa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and valid_cap next_capa and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap next_capa) (of_bl (drop (?a412 word nat list fun s' next_capa) cref)) (length cref - (nat + length list))) (CSpace_A.resolve_address_bits (next_capa, drop (nat + length list) cref))
 3. \<And>word nat list fun s' next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<not> Structures_A.is_cnode_cap next_capa \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and valid_cap next_capa and valid_global_refs and valid_idle and valid_etcbs) (returnOk ((word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)), length cref - (nat + length list))) (returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref))
 4. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 6. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (7 subgoals):
 1. \<And>word nat list fun s' next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; Structures_A.is_cnode_cap next_capa; ?a418 word nat list fun s' next_capa + ?b418 word nat list fun s' next_capa - ?a418 word nat list fun s' next_capa \<le> ?b418 word nat list fun s' next_capa\<rbrakk> \<Longrightarrow> ?a412 word nat list fun s' next_capa + (length cref - (nat + length list)) \<le> length cref \<and> length cref \<le> 32
 2. \<And>word nat list fun s' next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; Structures_A.is_cnode_cap next_capa\<rbrakk> \<Longrightarrow> ?a418 word nat list fun s' next_capa + ?b418 word nat list fun s' next_capa - ?a418 word nat list fun s' next_capa \<le> ?b418 word nat list fun s' next_capa
 3. \<And>word nat list fun s' next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; Structures_A.is_cnode_cap next_capa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and valid_cap next_capa and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap next_capa) (of_bl (drop (?a412 word nat list fun s' next_capa) cref)) (length cref - (nat + length list))) (CSpace_A.resolve_address_bits (next_capa, drop (nat + length list) cref))
 4. \<And>word nat list fun s' next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<not> Structures_A.is_cnode_cap next_capa \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and valid_cap next_capa and valid_global_refs and valid_idle and valid_etcbs) (returnOk ((word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)), length cref - (nat + length list))) (returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref))
 5. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 7. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (5 subgoals):
 1. \<And>word nat list fun s' next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; Structures_A.is_cnode_cap next_capa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and valid_cap next_capa and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap next_capa) (of_bl (drop (nat + length list) cref)) (length cref - (nat + length list))) (CSpace_A.resolve_address_bits (next_capa, drop (nat + length list) cref))
 2. \<And>word nat list fun s' next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<not> Structures_A.is_cnode_cap next_capa \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and valid_cap next_capa and valid_global_refs and valid_idle and valid_etcbs) (returnOk ((word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)), length cref - (nat + length list))) (returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref))
 3. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 5. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (5 subgoals):
 1. \<And>word nat list fun s' next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; Structures_A.is_cnode_cap next_capa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and valid_cap next_capa and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits (transform_cap next_capa) (of_bl (drop (nat + length list) cref)) (length (drop (nat + length list) cref))) (CSpace_A.resolve_address_bits (next_capa, drop (nat + length list) cref))
 2. \<And>word nat list fun s' next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<not> Structures_A.is_cnode_cap next_capa \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and valid_cap next_capa and valid_global_refs and valid_idle and valid_etcbs) (returnOk ((word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)), length cref - (nat + length list))) (returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref))
 3. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 5. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (5 subgoals):
 1. \<And>word nat list fun s' next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; Structures_A.is_cnode_cap next_capa\<rbrakk> \<Longrightarrow> length (drop (nat + length list) cref) \<le> m \<and> length (drop (nat + length list) cref) \<le> 32 \<and> transform_cap next_capa = transform_cap next_capa
 2. \<And>word nat list fun s' next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<not> Structures_A.is_cnode_cap next_capa \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and valid_cap next_capa and valid_global_refs and valid_idle and valid_etcbs) (returnOk ((word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)), length cref - (nat + length list))) (returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref))
 3. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 5. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (4 subgoals):
 1. \<And>word nat list fun s' next_capa. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s' word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<not> Structures_A.is_cnode_cap next_capa \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>s. True) (valid_objs and valid_cap next_capa and valid_global_refs and valid_idle and valid_etcbs) (returnOk ((word, unat ((of_bl cref >> length cref - (nat + length list)) && mask nat)), length cref - (nat + length list))) (returnOk ((word, take nat (drop (length list) cref)), drop (nat + length list) cref))
 2. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 4. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (4 subgoals):
 1. \<And>word nata list fun s' next_capa s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'; valid_idle s'; valid_etcbs s'; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nata; cap' = cap.CNodeCap word nata list; valid_objs s'; cap_aligned (cap.CNodeCap word nata list); 0 < nata; kheap s' word = Some (kernel_object.CNode nata fun); well_formed_cnode_n nata fun; nata + length list < length cref; list \<le> cref; \<not> Structures_A.is_cnode_cap next_capa; valid_objs s'a; s'a \<turnstile> next_capa; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a\<rbrakk> \<Longrightarrow> unat ((of_bl cref >> length cref - (nata + length list)) && mask nata) = nat (bl_to_bin (take nata (drop (length list) cref)))
 2. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 4. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal (3 subgoals):
 1. \<And>word nat list fun s'a s. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; transform s'a = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> KHeap_D.get_object word \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> KHeap_D.get_object word \<lbrace>\<lambda>x y. y = transform s'a \<and> x = transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun)\<rbrace>
 3. \<And>word nat list fun s'a. \<lbrakk>length list \<le> word_bits; valid_global_refs s'a; valid_idle s'a; valid_etcbs s'a; length cref \<le> Suc m; length cref \<le> 32; cap = cdl_cap.CNodeCap word (of_bl list) (length list) nat; cap' = cap.CNodeCap word nat list; valid_objs s'a; cap_aligned (cap.CNodeCap word nat list); 0 < nat; kheap s'a word = Some (kernel_object.CNode nat fun); well_formed_cnode_n nat fun; nat + length list < length cref; list \<le> cref; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s'a)) (KHeap_D.get_object word) proof (prove)
goal:
No subgoals! proof (state)
this:
length cref \<le> Suc m \<and> length cref \<le> 32 \<and> cap = transform_cap cap' \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) (\<lambda>_. True) (valid_objs and (\<lambda>a. a \<turnstile> cap') and valid_global_refs and valid_idle and valid_etcbs) (CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (CSpace_A.resolve_address_bits (cap', cref))

goal:
No subgoals!