theory Retype_DP

lemma invoke_untyped_preempt:
  "finite obj_range \<Longrightarrow>
  \<lbrace>cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>*
         sep_map_set_conj sep_any_map_o obj_range \<and>* Q)\<rbrace>
    invoke_untyped (Retype slot nt (unat ts) dests has_kids n)
   -, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift
         (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>*
         sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>" apply (simp add: invoke_untyped_def) apply (wp unlessE_wp) apply (simp add: reset_untyped_cap_def whenE_liftE | wp whenE_wp)+ apply (rule_tac P = "\<exists>a. cap = UntypedCap dev obj_range a" in hoare_gen_asmEx) apply (rule hoare_post_impErr[where E = E and F = E for E]) apply (rule mapME_x_inv_wp[where P = P and E = "\<lambda>r. P" for P]) apply wp apply simp apply (wp hoare_vcg_ex_lift) apply (rule hoare_post_imp[OF _ set_cap_wp]) apply sep_solve apply clarsimp apply (rule exI) apply sep_solve apply simp apply simp apply wp+ apply clarsimp apply (frule opt_cap_sep_imp) apply (clarsimp dest!: reset_cap_asid_untyped_cap_eqD) apply (cut_tac S = obj_range in detype_set_wp[unfolded bind_def valid_def simpler_modify_def]) apply simp apply (drule_tac x = s in spec) apply (erule impE) apply clarsimp apply sep_solve apply clarsimp apply (rule exI) apply sep_cancel+ apply (erule sep_map_set_conj_impl) apply sep_solve apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite obj_range \<Longrightarrow> \<lbrace>cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q)\<rbrace> invoke_untyped (Retype slot nt (unat ts) dests has_kids n) -, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q)\<rbrace> doE y <- unlessE has_kids (reset_untyped_cap slot);
liftE (do untyped_cap <- get_cap slot;
new_obj_refs <- generate_object_ids n nt (available_range untyped_cap);
y <- update_available_range (available_range untyped_cap) (map pick new_obj_refs) slot untyped_cap;
y <- retype_region (unat ts) nt new_obj_refs;
mapM_x (create_cap nt (unat ts) slot (untyped_is_device untyped_cap)) (zip dests new_obj_refs)
od)
odE -, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<not> has_kids \<Longrightarrow> \<lbrace>?Q12\<rbrace> reset_untyped_cap slot \<lbrace>\<lambda>y _. True\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 2. \<And>s. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s \<Longrightarrow> (if has_kids then \<lambda>_. True else ?Q12) s proof (prove)
goal (5 subgoals):
 1. \<And>cap x. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B17 cap () x\<rbrace> mapME_x (\<lambda>r. doE y <- liftE (set_cap slot (set_available_range cap r));
returnOk () \<sqinter> throw
odE) x \<lbrace>\<lambda>y _. True\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 2. \<And>cap y. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>?B17 cap y\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 3. \<And>cap. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B16 cap\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 4. \<not> has_kids \<Longrightarrow> \<lbrace>?Q12\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q15 cap else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 5. \<And>s. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s \<Longrightarrow> (if has_kids then \<lambda>_. True else ?Q12) s proof (prove)
goal (5 subgoals):
 1. \<And>cap x. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a\<rbrakk> \<Longrightarrow> \<lbrace>?P'24 cap () x\<rbrace> mapME_x (\<lambda>r. doE y <- liftE (set_cap slot (set_available_range cap r));
returnOk () \<sqinter> throw
odE) x \<lbrace>\<lambda>y _. True\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 2. \<And>cap y. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>a. ?P'24 cap y a and K (\<exists>a. cap = UntypedCap dev obj_range a)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 3. \<And>cap. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B16 cap\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 4. \<not> has_kids \<Longrightarrow> \<lbrace>?Q12\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q15 cap else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 5. \<And>s. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s \<Longrightarrow> (if has_kids then \<lambda>_. True else ?Q12) s proof (prove)
goal (7 subgoals):
 1. \<And>cap x. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a\<rbrakk> \<Longrightarrow> \<lbrace>?P'24 cap () x\<rbrace> mapME_x (\<lambda>r. doE y <- liftE (set_cap slot (set_available_range cap r));
returnOk () \<sqinter> throw
odE) x \<lbrace>?Q25 cap x\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 2. \<And>cap x rv s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; ?Q25 cap x rv s\<rbrakk> \<Longrightarrow> True
 3. \<And>cap x e s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s
 4. \<And>cap y. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>a. ?P'24 cap y a and K (\<exists>a. cap = UntypedCap dev obj_range a)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 5. \<And>cap. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B16 cap\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 6. \<not> has_kids \<Longrightarrow> \<lbrace>?Q12\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q15 cap else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 7. \<And>s. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s \<Longrightarrow> (if has_kids then \<lambda>_. True else ?Q12) s proof (prove)
goal (7 subgoals):
 1. \<And>cap x xa. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) a\<rbrace> doE y <- liftE (set_cap slot (set_available_range cap xa));
returnOk () \<sqinter> throw
odE \<lbrace>\<lambda>rv a. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) a\<rbrace>, \<lbrace>\<lambda>x a. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) a\<rbrace>
 2. \<And>cap x rv s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> True
 3. \<And>cap x e s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s
 4. \<And>cap y. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>a. (\<lambda>a. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) a) and K (\<exists>a. cap = UntypedCap dev obj_range a)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 5. \<And>cap. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B16 cap\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 6. \<not> has_kids \<Longrightarrow> \<lbrace>?Q12\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q15 cap else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 7. \<And>s. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s \<Longrightarrow> (if has_kids then \<lambda>_. True else ?Q12) s proof (prove)
goal (8 subgoals):
 1. \<And>cap x xa. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a\<rbrakk> \<Longrightarrow> \<lbrace>?Q44 cap x xa\<rbrace> set_cap slot (set_available_range cap xa) \<lbrace>\<lambda>xb s. (\<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s) \<and> (\<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s) \<and> True\<rbrace>
 2. \<And>cap x xa s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> ?Q44 cap x xa s
 3. \<And>cap x rv s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> True
 4. \<And>cap x e s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s
 5. \<And>cap y. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>a. (\<lambda>a. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) a) and K (\<exists>a. cap = UntypedCap dev obj_range a)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 6. \<And>cap. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B16 cap\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 7. \<not> has_kids \<Longrightarrow> \<lbrace>?Q12\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q15 cap else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 8. \<And>s. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s \<Longrightarrow> (if has_kids then \<lambda>_. True else ?Q12) s proof (prove)
goal (8 subgoals):
 1. \<And>cap x xa. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a\<rbrakk> \<Longrightarrow> \<lbrace>?Q44 cap x xa\<rbrace> set_cap slot (set_available_range cap xa) \<lbrace>\<lambda>xb s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 2. \<And>cap x xa s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> ?Q44 cap x xa s
 3. \<And>cap x rv s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> True
 4. \<And>cap x e s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s
 5. \<And>cap y. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>a. (\<lambda>a. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) a) and K (\<exists>a. cap = UntypedCap dev obj_range a)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 6. \<And>cap. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B16 cap\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 7. \<not> has_kids \<Longrightarrow> \<lbrace>?Q12\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q15 cap else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 8. \<And>s. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s \<Longrightarrow> (if has_kids then \<lambda>_. True else ?Q12) s proof (prove)
goal (8 subgoals):
 1. \<And>cap x xa free_range. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a\<rbrakk> \<Longrightarrow> \<lbrace>?P56 cap x xa free_range\<rbrace> set_cap slot (set_available_range cap xa) \<lbrace>\<lambda>rv. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q)\<rbrace>
 2. \<And>cap x xa s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> \<exists>xb. ?P56 cap x xa xb s
 3. \<And>cap x rv s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> True
 4. \<And>cap x e s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s
 5. \<And>cap y. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>a. (\<lambda>a. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) a) and K (\<exists>a. cap = UntypedCap dev obj_range a)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 6. \<And>cap. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B16 cap\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 7. \<not> has_kids \<Longrightarrow> \<lbrace>?Q12\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q15 cap else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 8. \<And>s. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s \<Longrightarrow> (if has_kids then \<lambda>_. True else ?Q12) s proof (prove)
goal (8 subgoals):
 1. \<And>cap x xa free_range rv s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; cdl.lift (slot \<mapsto>c set_available_range cap xa \<and>* ?R59 cap x xa free_range) s\<rbrakk> \<Longrightarrow> cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s
 2. \<And>cap x xa s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> \<exists>xb. cdl.lift (slot \<mapsto>c - \<and>* ?R59 cap x xa xb) s
 3. \<And>cap x rv s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> True
 4. \<And>cap x e s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s
 5. \<And>cap y. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>a. (\<lambda>a. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) a) and K (\<exists>a. cap = UntypedCap dev obj_range a)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 6. \<And>cap. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B16 cap\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 7. \<not> has_kids \<Longrightarrow> \<lbrace>?Q12\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q15 cap else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 8. \<And>s. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s \<Longrightarrow> (if has_kids then \<lambda>_. True else ?Q12) s proof (prove)
goal (7 subgoals):
 1. \<And>cap x xa s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> \<exists>x. cdl.lift (slot \<mapsto>c - \<and>* (slot \<mapsto>c set_available_range cap xa \<longrightarrow>* slot \<mapsto>c UntypedCap dev obj_range x \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q)) s
 2. \<And>cap x rv s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> True
 3. \<And>cap x e s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s
 4. \<And>cap y. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>a. (\<lambda>a. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) a) and K (\<exists>a. cap = UntypedCap dev obj_range a)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 5. \<And>cap. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B16 cap\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 6. \<not> has_kids \<Longrightarrow> \<lbrace>?Q12\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q15 cap else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 7. \<And>s. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s \<Longrightarrow> (if has_kids then \<lambda>_. True else ?Q12) s proof (prove)
goal (7 subgoals):
 1. \<And>xa s a free_range. \<lbrakk>\<not> has_kids; a \<noteq> obj_range; cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> \<exists>x. cdl.lift (slot \<mapsto>c - \<and>* (slot \<mapsto>c UntypedCap dev obj_range xa \<longrightarrow>* slot \<mapsto>c UntypedCap dev obj_range x \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q)) s
 2. \<And>cap x rv s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> True
 3. \<And>cap x e s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s
 4. \<And>cap y. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>a. (\<lambda>a. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) a) and K (\<exists>a. cap = UntypedCap dev obj_range a)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 5. \<And>cap. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B16 cap\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 6. \<not> has_kids \<Longrightarrow> \<lbrace>?Q12\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q15 cap else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 7. \<And>s. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s \<Longrightarrow> (if has_kids then \<lambda>_. True else ?Q12) s proof (prove)
goal (7 subgoals):
 1. \<And>xa s a free_range. \<lbrakk>\<not> has_kids; a \<noteq> obj_range; cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> cdl.lift (slot \<mapsto>c - \<and>* (slot \<mapsto>c UntypedCap dev obj_range xa \<longrightarrow>* slot \<mapsto>c UntypedCap dev obj_range (?x85 xa s a free_range) \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q)) s
 2. \<And>cap x rv s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> True
 3. \<And>cap x e s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s
 4. \<And>cap y. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>a. (\<lambda>a. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) a) and K (\<exists>a. cap = UntypedCap dev obj_range a)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 5. \<And>cap. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B16 cap\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 6. \<not> has_kids \<Longrightarrow> \<lbrace>?Q12\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q15 cap else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 7. \<And>s. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s \<Longrightarrow> (if has_kids then \<lambda>_. True else ?Q12) s proof (prove)
goal (6 subgoals):
 1. \<And>cap x rv s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> True
 2. \<And>cap x e s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s
 3. \<And>cap y. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>a. (\<lambda>a. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) a) and K (\<exists>a. cap = UntypedCap dev obj_range a)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 4. \<And>cap. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B16 cap\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 5. \<not> has_kids \<Longrightarrow> \<lbrace>?Q12\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q15 cap else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 6. \<And>s. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s \<Longrightarrow> (if has_kids then \<lambda>_. True else ?Q12) s proof (prove)
goal (5 subgoals):
 1. \<And>cap x e s. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap; \<exists>a. cap = UntypedCap dev obj_range a; \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s
 2. \<And>cap y. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>a. (\<lambda>a. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) a) and K (\<exists>a. cap = UntypedCap dev obj_range a)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 3. \<And>cap. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B16 cap\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 4. \<not> has_kids \<Longrightarrow> \<lbrace>?Q12\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q15 cap else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 5. \<And>s. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s \<Longrightarrow> (if has_kids then \<lambda>_. True else ?Q12) s proof (prove)
goal (4 subgoals):
 1. \<And>cap y. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B16 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>a. (\<lambda>a. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) a) and K (\<exists>a. cap = UntypedCap dev obj_range a)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 2. \<And>cap. \<lbrakk>\<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B16 cap\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 3. \<not> has_kids \<Longrightarrow> \<lbrace>?Q12\<rbrace> liftE (get_cap slot) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q15 cap else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>x s. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s\<rbrace>
 4. \<And>s. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s \<Longrightarrow> (if has_kids then \<lambda>_. True else ?Q12) s proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s \<Longrightarrow> (if has_kids then \<lambda>_. True else (\<lambda>s. opt_cap slot s \<noteq> None \<longrightarrow> (if available_range (the (opt_cap slot s)) \<noteq> cap_objects (the (opt_cap slot s)) then \<lambda>sa. \<forall>x\<in>{xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects (the (opt_cap slot s)) \<and> available_range (the (opt_cap slot s)) \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects (the (opt_cap slot s))}. ((\<lambda>a. \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) a) and K (\<exists>a. the (opt_cap slot s) = UntypedCap dev obj_range a)) (detype (cap_objects (the (opt_cap slot s))) sa) else (\<lambda>_. True)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s y x. \<lbrakk>cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s; available_range y \<noteq> cap_objects y; \<not> has_kids; opt_cap slot s = Some y; \<forall>S\<in>set x. S \<subseteq> cap_objects y \<and> available_range y \<subset> S; x \<noteq> []; last x = cap_objects y\<rbrakk> \<Longrightarrow> (\<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) (detype (cap_objects y) s)) \<and> (\<exists>a. y = UntypedCap dev obj_range a) proof (prove)
goal (1 subgoal):
 1. \<And>s y x. \<lbrakk>cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) s; available_range y \<noteq> cap_objects y; \<not> has_kids; opt_cap slot s = Some y; \<forall>S\<in>set x. S \<subseteq> cap_objects y \<and> available_range y \<subset> S; x \<noteq> []; last x = cap_objects y; \<exists>cap'. opt_cap slot s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid (UntypedCap dev obj_range free_range)\<rbrakk> \<Longrightarrow> (\<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev obj_range free_range \<and>* sep_map_set_conj sep_any_map_o obj_range \<and>* Q) (detype (cap_objects y) s)) \<and> (\<exists>a. y = UntypedCap dev obj_range a) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) s; free_range \<noteq> last x; \<not> has_kids; opt_cap slot s = Some (UntypedCap dev (last x) free_range); \<forall>S\<in>set x. S \<subseteq> last x \<and> free_range \<subset> S; x \<noteq> []; obj_range = last x\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) (detype (last x) s) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) s; free_range \<noteq> last x; \<not> has_kids; opt_cap slot s = Some (UntypedCap dev (last x) free_range); \<forall>S\<in>set x. S \<subseteq> last x \<and> free_range \<subset> S; x \<noteq> []; obj_range = last x\<rbrakk> \<Longrightarrow> finite obj_range
 2. \<And>s x. \<lbrakk>cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) s; free_range \<noteq> last x; \<not> has_kids; opt_cap slot s = Some (UntypedCap dev (last x) free_range); \<forall>S\<in>set x. S \<subseteq> last x \<and> free_range \<subset> S; x \<noteq> []; obj_range = last x; \<forall>sa. cdl.lift (sep_map_set_conj sep_any_map_o obj_range \<and>* ?R137 s x) sa \<longrightarrow> (\<forall>(r, s')\<in>fst ({((), detype obj_range sa)}, False). cdl.lift ((SETSEPCONJ x:obj_range. x \<mapsto>o Untyped) \<and>* ?R137 s x) s')\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) (detype (last x) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) s; free_range \<noteq> last x; \<not> has_kids; opt_cap slot s = Some (UntypedCap dev (last x) free_range); \<forall>S\<in>set x. S \<subseteq> last x \<and> free_range \<subset> S; x \<noteq> []; obj_range = last x; \<forall>sa. cdl.lift (sep_map_set_conj sep_any_map_o obj_range \<and>* ?R137 s x) sa \<longrightarrow> (\<forall>(r, s')\<in>fst ({((), detype obj_range sa)}, False). cdl.lift ((SETSEPCONJ x:obj_range. x \<mapsto>o Untyped) \<and>* ?R137 s x) s')\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) (detype (last x) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) s; free_range \<noteq> last x; \<not> has_kids; opt_cap slot s = Some (UntypedCap dev (last x) free_range); \<forall>S\<in>set x. S \<subseteq> last x \<and> free_range \<subset> S; x \<noteq> []; obj_range = last x; cdl.lift (sep_map_set_conj sep_any_map_o obj_range \<and>* ?R137 s x) s \<longrightarrow> (\<forall>(r, s')\<in>fst ({((), detype obj_range s)}, False). cdl.lift ((SETSEPCONJ x:obj_range. x \<mapsto>o Untyped) \<and>* ?R137 s x) s')\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) (detype (last x) s) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) s; free_range \<noteq> last x; \<not> has_kids; opt_cap slot s = Some (UntypedCap dev (last x) free_range); \<forall>S\<in>set x. S \<subseteq> last x \<and> free_range \<subset> S; x \<noteq> []; obj_range = last x\<rbrakk> \<Longrightarrow> cdl.lift (sep_map_set_conj sep_any_map_o obj_range \<and>* ?R137 s x) s
 2. \<And>s x. \<lbrakk>cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) s; free_range \<noteq> last x; \<not> has_kids; opt_cap slot s = Some (UntypedCap dev (last x) free_range); \<forall>S\<in>set x. S \<subseteq> last x \<and> free_range \<subset> S; x \<noteq> []; obj_range = last x; \<forall>(r, s')\<in>fst ({((), detype obj_range s)}, False). cdl.lift ((SETSEPCONJ x:obj_range. x \<mapsto>o Untyped) \<and>* ?R137 s x) s'\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) (detype (last x) s) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) s; free_range \<noteq> last x; \<not> has_kids; opt_cap slot s = Some (UntypedCap dev (last x) free_range); \<forall>S\<in>set x. S \<subseteq> last x \<and> free_range \<subset> S; x \<noteq> []; obj_range = last x\<rbrakk> \<Longrightarrow> cdl.lift (sep_map_set_conj sep_any_map_o (last x) \<and>* ?R137 s x) s
 2. \<And>s x. \<lbrakk>cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) s; free_range \<noteq> last x; \<not> has_kids; opt_cap slot s = Some (UntypedCap dev (last x) free_range); \<forall>S\<in>set x. S \<subseteq> last x \<and> free_range \<subset> S; x \<noteq> []; obj_range = last x; \<forall>(r, s')\<in>fst ({((), detype obj_range s)}, False). cdl.lift ((SETSEPCONJ x:obj_range. x \<mapsto>o Untyped) \<and>* ?R137 s x) s'\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) (detype (last x) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) s; free_range \<noteq> last x; \<not> has_kids; opt_cap slot s = Some (UntypedCap dev (last x) free_range); \<forall>S\<in>set x. S \<subseteq> last x \<and> free_range \<subset> S; x \<noteq> []; obj_range = last x; \<forall>(r, s')\<in>fst ({((), detype obj_range s)}, False). cdl.lift ((SETSEPCONJ x:obj_range. x \<mapsto>o Untyped) \<and>* slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* Q) s'\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) (detype (last x) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) s; free_range \<noteq> last x; \<not> has_kids; opt_cap slot s = Some (UntypedCap dev (last x) free_range); \<forall>S\<in>set x. S \<subseteq> last x \<and> free_range \<subset> S; x \<noteq> []; obj_range = last x; cdl.lift ((SETSEPCONJ x:last x. x \<mapsto>o Untyped) \<and>* slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* Q) (detype (last x) s)\<rbrakk> \<Longrightarrow> \<exists>free_range. cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) (detype (last x) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) s; free_range \<noteq> last x; \<not> has_kids; opt_cap slot s = Some (UntypedCap dev (last x) free_range); \<forall>S\<in>set x. S \<subseteq> last x \<and> free_range \<subset> S; x \<noteq> []; obj_range = last x; cdl.lift ((SETSEPCONJ x:last x. x \<mapsto>o Untyped) \<and>* slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* Q) (detype (last x) s)\<rbrakk> \<Longrightarrow> cdl.lift (slot \<mapsto>c UntypedCap dev (last x) (?free_range158 s x) \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) (detype (last x) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x sa sb. \<lbrakk>cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) s; free_range \<noteq> last x; \<not> has_kids; opt_cap slot s = Some (UntypedCap dev (last x) free_range); \<forall>S\<in>set x. S \<subseteq> last x \<and> free_range \<subset> S; x \<noteq> []; obj_range = last x; (SETSEPCONJ x:last x. x \<mapsto>o Untyped) sb\<rbrakk> \<Longrightarrow> sep_map_set_conj sep_any_map_o (last x) sb proof (prove)
goal (2 subgoals):
 1. \<And>s x sa sb sc xa. \<lbrakk>cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) s; free_range \<noteq> last x; \<not> has_kids; opt_cap slot s = Some (UntypedCap dev (last x) free_range); \<forall>S\<in>set x. S \<subseteq> last x \<and> free_range \<subset> S; x \<noteq> []; obj_range = last x; xa \<in> last x; (xa \<mapsto>o Untyped) sc\<rbrakk> \<Longrightarrow> (xa \<mapsto>o -) sc
 2. \<And>s x sa sb. \<lbrakk>cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) s; free_range \<noteq> last x; \<not> has_kids; opt_cap slot s = Some (UntypedCap dev (last x) free_range); \<forall>S\<in>set x. S \<subseteq> last x \<and> free_range \<subset> S; x \<noteq> []; obj_range = last x\<rbrakk> \<Longrightarrow> finite (last x) proof (prove)
goal (1 subgoal):
 1. \<And>s x sa sb. \<lbrakk>cdl.lift (slot \<mapsto>c UntypedCap dev (last x) free_range \<and>* sep_map_set_conj sep_any_map_o (last x) \<and>* Q) s; free_range \<noteq> last x; \<not> has_kids; opt_cap slot s = Some (UntypedCap dev (last x) free_range); \<forall>S\<in>set x. S \<subseteq> last x \<and> free_range \<subset> S; x \<noteq> []; obj_range = last x\<rbrakk> \<Longrightarrow> finite (last x) proof (prove)
goal:
No subgoals!