theory CNode_DR

lemma dcorres_set_untyped_cap_as_full:
  "dcorres dc \<top> (K (cap_aligned cap) and cte_wp_at ((=) src_cap) src
  and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs)
  (CSpace_D.set_untyped_cap_as_full (transform_cap src_cap) (transform_cap cap) (transform_cslot_ptr src))
  (CSpace_A.set_untyped_cap_as_full src_cap cap src)" apply (simp add:set_untyped_cap_as_full_def CSpace_D.set_untyped_cap_as_full_def
              split del:if_split) apply (case_tac "is_untyped_cap src_cap \<and> is_untyped_cap cap") apply (rule dcorres_expand_pfx) apply (rule corres_guard_imp) apply (rule corres_if) apply clarsimp apply (clarsimp dest!:is_untyped_cap_eqD) apply (drule(1) cte_wp_valid_cap) apply (simp add:valid_cap_def cap_aligned_def) apply (rule iffI) apply clarsimp apply (drule two_power_eq[THEN iffD1,rotated 2]) apply (simp add:valid_cap_def word_bits_def cap_aligned_def) apply (simp add:valid_cap_def word_bits_def cap_aligned_def) apply simp apply simp apply (rule_tac F = "is_untyped_cap src_cap \<and> is_untyped_cap cap"  in corres_gen_asm) apply (clarsimp dest!:is_untyped_cap_eqD) apply (rule set_cap_corres) apply (clarsimp simp:transform_cap_def free_range_of_untyped_def cap_aligned_def max_free_index_def
                       dest!:is_untyped_cap_eqD) apply (cut_tac sz = sz in p2_less_minus) apply simp apply simp apply simp apply fastforce apply (fastforce simp:not_idle_thread_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (K (cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (CSpace_D.set_untyped_cap_as_full (transform_cap src_cap) (transform_cap cap) (transform_cslot_ptr src)) (CSpace_A.set_untyped_cap_as_full src_cap cap src) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (2 subgoals):
 1. Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ())
 2. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ())
 2. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q5 s s') (?Q'5 s s') (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ())
 2. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> ?Q5 s s' sa
 3. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> ?Q'5 s s' sa
 4. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (6 subgoals):
 1. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap)) = (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap)
 2. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?P9 s s') (?P'9 s s') (KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {})) (CSpaceAcc_A.set_cap (max_free_index_update src_cap) src)
 3. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 4. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then ?P9 s s' else ?Q9 s s') sa
 5. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then ?P'9 s s' else ?Q'9 s s') sa
 6. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>Structures_A.is_untyped_cap src_cap; Structures_A.is_untyped_cap cap; cap_aligned cap; cte_wp_at ((=) src_cap) src s'; valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap)) = (obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap)
 2. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?P9 s s') (?P'9 s s') (KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {})) (CSpaceAcc_A.set_cap (max_free_index_update src_cap) src)
 3. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 4. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then ?P9 s s' else ?Q9 s s') sa
 5. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then ?P'9 s s' else ?Q'9 s s') sa
 6. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (6 subgoals):
 1. \<And>s' dev deva ptr ptra sz sza idx idxa. \<lbrakk>cap_aligned (cap.UntypedCap deva ptra sza idxa); cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) src s'; valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptra sza idxa\<rbrakk> \<Longrightarrow> (ptr = ptra \<and> ptr + 2 ^ sz = ptra + 2 ^ sza \<or> \<not> ptr \<le> ptr + 2 ^ sz - 1 \<and> \<not> ptra \<le> ptra + 2 ^ sza - 1) = (ptr = ptra \<and> sz = sza)
 2. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?P9 s s') (?P'9 s s') (KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {})) (CSpaceAcc_A.set_cap (max_free_index_update src_cap) src)
 3. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 4. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then ?P9 s s' else ?Q9 s s') sa
 5. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then ?P'9 s s' else ?Q'9 s s') sa
 6. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (6 subgoals):
 1. \<And>s' dev deva ptr ptra sz sza idx idxa. \<lbrakk>cap_aligned (cap.UntypedCap deva ptra sza idxa); valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptra sza idxa; s' \<turnstile> cap.UntypedCap dev ptr sz idx\<rbrakk> \<Longrightarrow> (ptr = ptra \<and> ptr + 2 ^ sz = ptra + 2 ^ sza \<or> \<not> ptr \<le> ptr + 2 ^ sz - 1 \<and> \<not> ptra \<le> ptra + 2 ^ sza - 1) = (ptr = ptra \<and> sz = sza)
 2. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?P9 s s') (?P'9 s s') (KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {})) (CSpaceAcc_A.set_cap (max_free_index_update src_cap) src)
 3. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 4. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then ?P9 s s' else ?Q9 s s') sa
 5. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then ?P'9 s s' else ?Q'9 s s') sa
 6. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (6 subgoals):
 1. \<And>s' dev deva ptr ptra sz sza idx idxa. \<lbrakk>is_aligned ptra sza \<and> sza < word_bits; valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptra sza idxa; is_aligned ptr sz \<and> sz < word_bits \<and> valid_untyped (cap.UntypedCap dev ptr sz idx) s' \<and> untyped_min_bits \<le> sz \<and> idx \<le> 2 ^ sz \<and> ptr \<noteq> 0\<rbrakk> \<Longrightarrow> (ptr = ptra \<and> ptr + 2 ^ sz = ptra + 2 ^ sza) = (ptr = ptra \<and> sz = sza)
 2. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?P9 s s') (?P'9 s s') (KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {})) (CSpaceAcc_A.set_cap (max_free_index_update src_cap) src)
 3. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 4. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then ?P9 s s' else ?Q9 s s') sa
 5. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then ?P'9 s s' else ?Q'9 s s') sa
 6. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (7 subgoals):
 1. \<And>s' dev deva ptr ptra sz sza idx idxa. \<lbrakk>is_aligned ptra sza \<and> sza < word_bits; valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptra sza idxa; is_aligned ptr sz \<and> sz < word_bits \<and> valid_untyped (cap.UntypedCap dev ptr sz idx) s' \<and> untyped_min_bits \<le> sz \<and> idx \<le> 2 ^ sz \<and> ptr \<noteq> 0; ptr = ptra \<and> ptr + 2 ^ sz = ptra + 2 ^ sza\<rbrakk> \<Longrightarrow> ptr = ptra \<and> sz = sza
 2. \<And>s' dev deva ptr ptra sz sza idx idxa. \<lbrakk>is_aligned ptra sza \<and> sza < word_bits; valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptra sza idxa; is_aligned ptr sz \<and> sz < word_bits \<and> valid_untyped (cap.UntypedCap dev ptr sz idx) s' \<and> untyped_min_bits \<le> sz \<and> idx \<le> 2 ^ sz \<and> ptr \<noteq> 0; ptr = ptra \<and> sz = sza\<rbrakk> \<Longrightarrow> ptr = ptra \<and> ptr + 2 ^ sz = ptra + 2 ^ sza
 3. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?P9 s s') (?P'9 s s') (KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {})) (CSpaceAcc_A.set_cap (max_free_index_update src_cap) src)
 4. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 5. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then ?P9 s s' else ?Q9 s s') sa
 6. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then ?P'9 s s' else ?Q'9 s s') sa
 7. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (7 subgoals):
 1. \<And>s' dev deva ptr sz sza idx idxa. \<lbrakk>valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptr sza idxa; 2 ^ sz = 2 ^ sza; is_aligned ptr sza; sza < word_bits; is_aligned ptr sz; sz < word_bits; valid_untyped (cap.UntypedCap dev ptr sz idx) s'; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> sz = sza
 2. \<And>s' dev deva ptr ptra sz sza idx idxa. \<lbrakk>is_aligned ptra sza \<and> sza < word_bits; valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptra sza idxa; is_aligned ptr sz \<and> sz < word_bits \<and> valid_untyped (cap.UntypedCap dev ptr sz idx) s' \<and> untyped_min_bits \<le> sz \<and> idx \<le> 2 ^ sz \<and> ptr \<noteq> 0; ptr = ptra \<and> sz = sza\<rbrakk> \<Longrightarrow> ptr = ptra \<and> ptr + 2 ^ sz = ptra + 2 ^ sza
 3. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?P9 s s') (?P'9 s s') (KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {})) (CSpaceAcc_A.set_cap (max_free_index_update src_cap) src)
 4. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 5. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then ?P9 s s' else ?Q9 s s') sa
 6. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then ?P'9 s s' else ?Q'9 s s') sa
 7. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (9 subgoals):
 1. \<And>s' dev deva ptr sz sza idx idxa. \<lbrakk>valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptr sza idxa; is_aligned ptr sza; sza < word_bits; is_aligned ptr sz; sz < word_bits; valid_untyped (cap.UntypedCap dev ptr sz idx) s'; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> sz < LENGTH(32)
 2. \<And>s' dev deva ptr sz sza idx idxa. \<lbrakk>valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptr sza idxa; is_aligned ptr sza; sza < word_bits; is_aligned ptr sz; sz < word_bits; valid_untyped (cap.UntypedCap dev ptr sz idx) s'; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> sza < LENGTH(32)
 3. \<And>s' dev deva ptr sz sza idx idxa. \<lbrakk>valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptr sza idxa; is_aligned ptr sza; sza < word_bits; is_aligned ptr sz; sz < word_bits; valid_untyped (cap.UntypedCap dev ptr sz idx) s'; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr \<noteq> 0; sz = sza\<rbrakk> \<Longrightarrow> sz = sza
 4. \<And>s' dev deva ptr ptra sz sza idx idxa. \<lbrakk>is_aligned ptra sza \<and> sza < word_bits; valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptra sza idxa; is_aligned ptr sz \<and> sz < word_bits \<and> valid_untyped (cap.UntypedCap dev ptr sz idx) s' \<and> untyped_min_bits \<le> sz \<and> idx \<le> 2 ^ sz \<and> ptr \<noteq> 0; ptr = ptra \<and> sz = sza\<rbrakk> \<Longrightarrow> ptr = ptra \<and> ptr + 2 ^ sz = ptra + 2 ^ sza
 5. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?P9 s s') (?P'9 s s') (KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {})) (CSpaceAcc_A.set_cap (max_free_index_update src_cap) src)
 6. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 7. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then ?P9 s s' else ?Q9 s s') sa
 8. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then ?P'9 s s' else ?Q'9 s s') sa
 9. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (8 subgoals):
 1. \<And>s' dev deva ptr sz sza idx idxa. \<lbrakk>valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptr sza idxa; is_aligned ptr sza; sza < word_bits; is_aligned ptr sz; sz < word_bits; valid_untyped (cap.UntypedCap dev ptr sz idx) s'; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> sza < LENGTH(32)
 2. \<And>s' dev deva ptr sz sza idx idxa. \<lbrakk>valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptr sza idxa; is_aligned ptr sza; sza < word_bits; is_aligned ptr sz; sz < word_bits; valid_untyped (cap.UntypedCap dev ptr sz idx) s'; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr \<noteq> 0; sz = sza\<rbrakk> \<Longrightarrow> sz = sza
 3. \<And>s' dev deva ptr ptra sz sza idx idxa. \<lbrakk>is_aligned ptra sza \<and> sza < word_bits; valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptra sza idxa; is_aligned ptr sz \<and> sz < word_bits \<and> valid_untyped (cap.UntypedCap dev ptr sz idx) s' \<and> untyped_min_bits \<le> sz \<and> idx \<le> 2 ^ sz \<and> ptr \<noteq> 0; ptr = ptra \<and> sz = sza\<rbrakk> \<Longrightarrow> ptr = ptra \<and> ptr + 2 ^ sz = ptra + 2 ^ sza
 4. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?P9 s s') (?P'9 s s') (KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {})) (CSpaceAcc_A.set_cap (max_free_index_update src_cap) src)
 5. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 6. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then ?P9 s s' else ?Q9 s s') sa
 7. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then ?P'9 s s' else ?Q'9 s s') sa
 8. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (7 subgoals):
 1. \<And>s' dev deva ptr sz sza idx idxa. \<lbrakk>valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptr sza idxa; is_aligned ptr sza; sza < word_bits; is_aligned ptr sz; sz < word_bits; valid_untyped (cap.UntypedCap dev ptr sz idx) s'; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr \<noteq> 0; sz = sza\<rbrakk> \<Longrightarrow> sz = sza
 2. \<And>s' dev deva ptr ptra sz sza idx idxa. \<lbrakk>is_aligned ptra sza \<and> sza < word_bits; valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptra sza idxa; is_aligned ptr sz \<and> sz < word_bits \<and> valid_untyped (cap.UntypedCap dev ptr sz idx) s' \<and> untyped_min_bits \<le> sz \<and> idx \<le> 2 ^ sz \<and> ptr \<noteq> 0; ptr = ptra \<and> sz = sza\<rbrakk> \<Longrightarrow> ptr = ptra \<and> ptr + 2 ^ sz = ptra + 2 ^ sza
 3. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?P9 s s') (?P'9 s s') (KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {})) (CSpaceAcc_A.set_cap (max_free_index_update src_cap) src)
 4. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 5. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then ?P9 s s' else ?Q9 s s') sa
 6. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then ?P'9 s s' else ?Q'9 s s') sa
 7. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (6 subgoals):
 1. \<And>s' dev deva ptr ptra sz sza idx idxa. \<lbrakk>is_aligned ptra sza \<and> sza < word_bits; valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptra sza idxa; is_aligned ptr sz \<and> sz < word_bits \<and> valid_untyped (cap.UntypedCap dev ptr sz idx) s' \<and> untyped_min_bits \<le> sz \<and> idx \<le> 2 ^ sz \<and> ptr \<noteq> 0; ptr = ptra \<and> sz = sza\<rbrakk> \<Longrightarrow> ptr = ptra \<and> ptr + 2 ^ sz = ptra + 2 ^ sza
 2. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?P9 s s') (?P'9 s s') (KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {})) (CSpaceAcc_A.set_cap (max_free_index_update src_cap) src)
 3. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 4. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then ?P9 s s' else ?Q9 s s') sa
 5. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then ?P'9 s s' else ?Q'9 s s') sa
 6. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (5 subgoals):
 1. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?P9 s s') (?P'9 s s') (KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {})) (CSpaceAcc_A.set_cap (max_free_index_update src_cap) src)
 2. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 3. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then ?P9 s s' else ?Q9 s s') sa
 4. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then ?P'9 s s' else ?Q'9 s s') sa
 5. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (5 subgoals):
 1. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap\<rbrakk> \<Longrightarrow> dcorres dc (?P56 s s') (?P'9 s s') (KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {})) (CSpaceAcc_A.set_cap (max_free_index_update src_cap) src)
 2. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 3. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then ?P56 s s' and (\<lambda>s. Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) else ?Q9 s s') sa
 4. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then ?P'9 s s' else ?Q'9 s s') sa
 5. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (5 subgoals):
 1. \<And>s' dev deva ptr ptra sz sza idx idxa. \<lbrakk>cap_aligned (cap.UntypedCap deva ptra sza idxa); src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptra sza idxa; cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) src s'; valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc (?P56 (transform s') s') (?P'9 (transform s') s') (KHeap_D.set_cap (transform_cslot_ptr src) (cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} {})) (CSpaceAcc_A.set_cap (cap.UntypedCap dev ptr sz (max_free_index sz)) src)
 2. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 3. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then ?P56 s s' and (\<lambda>s. Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) else ?Q9 s s') sa
 4. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then ?P'9 s s' else ?Q'9 s s') sa
 5. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (6 subgoals):
 1. \<And>s' dev deva ptr ptra sz sza idx idxa. \<lbrakk>cap_aligned (cap.UntypedCap deva ptra sza idxa); src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptra sza idxa; cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) src s'; valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> cdl_cap.UntypedCap dev {ptr..ptr + 2 ^ sz - 1} {} = transform_cap (cap.UntypedCap dev ptr sz (max_free_index sz))
 2. \<And>s' dev deva ptr ptra sz sza idx idxa. \<lbrakk>cap_aligned (cap.UntypedCap deva ptra sza idxa); src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptra sza idxa; cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) src s'; valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> transform_cslot_ptr src = transform_cslot_ptr src
 3. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 4. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then (\<lambda>a. True) and (\<lambda>s. Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) else ?Q9 s s') sa
 5. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then \<lambda>a. valid_idle a \<and> fst src \<noteq> idle_thread a \<and> valid_etcbs a else ?Q'9 s s') sa
 6. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (6 subgoals):
 1. \<And>s' dev deva ptr ptra sz sza idx idxa. \<lbrakk>src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptra sza idxa; cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) src s'; valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; is_aligned ptra sza; sza < word_bits; 2 ^ sz \<le> 2 ^ sz - Suc 0; ptr + 2 ^ sz \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> False
 2. \<And>s' dev deva ptr ptra sz sza idx idxa. \<lbrakk>cap_aligned (cap.UntypedCap deva ptra sza idxa); src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptra sza idxa; cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) src s'; valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> transform_cslot_ptr src = transform_cslot_ptr src
 3. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 4. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then (\<lambda>a. True) and (\<lambda>s. Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) else ?Q9 s s') sa
 5. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then \<lambda>a. valid_idle a \<and> fst src \<noteq> idle_thread a \<and> valid_etcbs a else ?Q'9 s s') sa
 6. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (6 subgoals):
 1. \<And>s' dev deva ptr ptra sz sza idx idxa. \<lbrakk>src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptra sza idxa; cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) src s'; valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'; is_aligned ptra sza; sza < word_bits; 2 ^ sz \<le> 2 ^ sz - Suc 0; ptr + 2 ^ sz \<le> ptr + 2 ^ sz - 1; 2 ^ sz - Suc 0 < 2 ^ sz\<rbrakk> \<Longrightarrow> False
 2. \<And>s' dev deva ptr ptra sz sza idx idxa. \<lbrakk>cap_aligned (cap.UntypedCap deva ptra sza idxa); src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptra sza idxa; cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) src s'; valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> transform_cslot_ptr src = transform_cslot_ptr src
 3. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 4. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then (\<lambda>a. True) and (\<lambda>s. Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) else ?Q9 s s') sa
 5. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then \<lambda>a. valid_idle a \<and> fst src \<noteq> idle_thread a \<and> valid_etcbs a else ?Q'9 s s') sa
 6. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (5 subgoals):
 1. \<And>s' dev deva ptr ptra sz sza idx idxa. \<lbrakk>cap_aligned (cap.UntypedCap deva ptra sza idxa); src_cap = cap.UntypedCap dev ptr sz idx; cap = cap.UntypedCap deva ptra sza idxa; cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) src s'; valid_objs s'; not_idle_thread (fst src) s'; valid_idle s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> transform_cslot_ptr src = transform_cslot_ptr src
 2. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 3. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then (\<lambda>a. True) and (\<lambda>s. Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) else ?Q9 s s') sa
 4. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then \<lambda>a. valid_idle a \<and> fst src \<noteq> idle_thread a \<and> valid_etcbs a else ?Q'9 s s') sa
 5. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q9 s s') (?Q'9 s s') (return ()) (return ())
 2. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then (\<lambda>a. True) and (\<lambda>s. Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) else ?Q9 s s') sa
 3. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then \<lambda>a. valid_idle a \<and> fst src \<noteq> idle_thread a \<and> valid_etcbs a else ?Q'9 s s') sa
 4. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (3 subgoals):
 1. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then (\<lambda>a. True) and (\<lambda>s. Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) else ?Q9 s s') sa
 2. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then \<lambda>a. valid_idle a \<and> fst src \<noteq> idle_thread a \<and> valid_etcbs a else ?Q'9 s s') sa
 3. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa. \<lbrakk>Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap; s = transform s'; True; ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then \<lambda>a. valid_idle a \<and> fst src \<noteq> idle_thread a \<and> valid_etcbs a else ?Q'9 s s') sa
 2. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal (1 subgoal):
 1. \<not> (Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap) \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>y. cap_aligned cap) and cte_wp_at ((=) src_cap) src and valid_objs and not_idle_thread (fst src) and valid_idle and valid_etcbs) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> cap_objects (transform_cap src_cap) = cap_objects (transform_cap cap) then KHeap_D.set_cap (transform_cslot_ptr src) (set_available_range (transform_cap src_cap) {}) else return ()) (if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then CSpaceAcc_A.set_cap (max_free_index_update src_cap) src else return ()) proof (prove)
goal:
No subgoals!