theory Retype_DP

lemma invoke_untyped_exception:
  "uinv = (Retype uref nt ts [dest_slot] has_kids (Suc 0))
  \<Longrightarrow> \<lbrace>K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType
     \<and> free_range \<subseteq> tot_free_range
     \<and> (\<not> retype_with_kids (InvokeUntyped uinv) \<longrightarrow> free_range = obj_range) \<and> finite tot_free_range)
     and (\<lambda>s. cdl_current_domain s = minBound)
     and < dest_slot \<mapsto>c NullCap
    \<and>* (\<And>* ptr\<in>tot_free_range. ptr \<mapsto>o Untyped)
    \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range
    \<and>* P > \<rbrace>
   invoke_untyped uinv -,\<lbrace>\<lambda>r. Q\<rbrace>" apply (simp add: invoke_untyped_def validE_E_def) apply (rule hoare_name_pre_stateE) apply (cases uinv) apply clarsimp apply (wp unlessE_wp
          | wpc | simp add: reset_untyped_cap_def)+ apply (rule_tac P = "available_range cap = cap_objects cap" in hoare_gen_asmEx) apply (simp add: whenE_def) apply wp+ apply clarsimp apply (cut_tac p = "uref" in opt_cap_sep_imp) apply sep_solve apply (clarsimp dest!: reset_cap_asid_simps2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>K (default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> free_range \<subseteq> tot_free_range \<and> (\<not> (case InvokeUntyped uinv of InvokeUntyped (Retype uref nt ts dest has_kids n) \<Rightarrow> has_kids) \<longrightarrow> free_range = obj_range) \<and> finite tot_free_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)\<rbrace> invoke_untyped uinv -, \<lbrace>\<lambda>r. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>(\<lambda>y. default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range)) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)\<rbrace> doE y <- unlessE has_kids (reset_untyped_cap uref);
liftE (do untyped_cap <- get_cap uref;
new_obj_refs <- generate_object_ids (Suc 0) nt (available_range untyped_cap);
y <- update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap;
y <- retype_region ts nt new_obj_refs;
mapM_x (create_cap nt ts uref (untyped_is_device untyped_cap)) (zip [dest_slot] new_obj_refs)
od)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); ((\<lambda>y. default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range)) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- unlessE has_kids (reset_untyped_cap uref);
liftE (do untyped_cap <- get_cap uref;
new_obj_refs <- generate_object_ids (Suc 0) nt (available_range untyped_cap);
y <- update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap;
y <- retype_region ts nt new_obj_refs;
mapM_x (create_cap nt ts uref (untyped_is_device untyped_cap)) (zip [dest_slot] new_obj_refs)
od)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2 x3 x4 x5 x6. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); ((\<lambda>y. default_object nt ts minBound = Some obj \<and> nt \<noteq> UntypedType \<and> free_range \<subseteq> tot_free_range \<and> (\<not> has_kids \<longrightarrow> free_range = obj_range)) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P)) s; uinv = Retype x1 x2 x3 x4 x5 x6\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- unlessE has_kids (reset_untyped_cap uref);
liftE (do untyped_cap <- get_cap uref;
new_obj_refs <- generate_object_ids (Suc 0) nt (available_range untyped_cap);
y <- update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap;
y <- retype_region ts nt new_obj_refs;
mapM_x (create_cap nt ts uref (untyped_is_device untyped_cap)) (zip [dest_slot] new_obj_refs)
od)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- unlessE has_kids (reset_untyped_cap uref);
liftE (do untyped_cap <- get_cap uref;
new_obj_refs <- generate_object_ids (Suc 0) nt (available_range untyped_cap);
y <- update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap;
y <- retype_region ts nt new_obj_refs;
mapM_x (create_cap nt ts uref (untyped_is_device untyped_cap)) (zip [dest_slot] new_obj_refs)
od)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s cap x. \<lbrakk>uinv = Retype uref nt ts [dest_slot] False (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; obj_range \<subseteq> tot_free_range; free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* P) s; \<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B25 s cap () x\<rbrace> mapME_x (\<lambda>r. doE y <- liftE (set_cap uref (set_available_range cap r));
returnOk () \<sqinter> throw
odE) x \<lbrace>\<lambda>y _. True\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace>
 2. \<And>s cap y. \<lbrakk>uinv = Retype uref nt ts [dest_slot] False (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; obj_range \<subseteq> tot_free_range; free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* P) s; \<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B24 s 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>?B25 s cap y\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace>
 3. \<And>s cap. \<lbrakk>uinv = Retype uref nt ts [dest_slot] False (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; obj_range \<subseteq> tot_free_range; free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* P) s; \<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 s cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B24 s cap\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace>
 4. \<And>s. \<lbrakk>uinv = Retype uref nt ts [dest_slot] False (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; obj_range \<subseteq> tot_free_range; free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* P) s; \<not> has_kids\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 s\<rbrace> liftE (get_cap uref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q23 s cap else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace>
 5. \<And>s sa. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> (if has_kids then \<lambda>_. True else ?Q17 s) sa proof (prove)
goal (5 subgoals):
 1. \<And>s cap x. \<lbrakk>uinv = Retype uref nt ts [dest_slot] False (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; obj_range \<subseteq> tot_free_range; free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* P) s; \<not> has_kids; available_range cap \<noteq> cap_objects cap; available_range cap = cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'29 s cap () x\<rbrace> mapME_x (\<lambda>r. doE y <- liftE (set_cap uref (set_available_range cap r));
returnOk () \<sqinter> throw
odE) x \<lbrace>\<lambda>y _. True\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace>
 2. \<And>s cap y. \<lbrakk>uinv = Retype uref nt ts [dest_slot] False (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; obj_range \<subseteq> tot_free_range; free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* P) s; \<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B24 s 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'29 s cap y a and K (available_range cap = cap_objects cap)\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace>
 3. \<And>s cap. \<lbrakk>uinv = Retype uref nt ts [dest_slot] False (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; obj_range \<subseteq> tot_free_range; free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* P) s; \<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 s cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B24 s cap\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace>
 4. \<And>s. \<lbrakk>uinv = Retype uref nt ts [dest_slot] False (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; obj_range \<subseteq> tot_free_range; free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* P) s; \<not> has_kids\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 s\<rbrace> liftE (get_cap uref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q23 s cap else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace>
 5. \<And>s sa. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> (if has_kids then \<lambda>_. True else ?Q17 s) sa proof (prove)
goal (4 subgoals):
 1. \<And>s cap y. \<lbrakk>uinv = Retype uref nt ts [dest_slot] False (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; obj_range \<subseteq> tot_free_range; free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* P) s; \<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?B24 s 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'29 s cap y a and K (available_range cap = cap_objects cap)\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace>
 2. \<And>s cap. \<lbrakk>uinv = Retype uref nt ts [dest_slot] False (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; obj_range \<subseteq> tot_free_range; free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* P) s; \<not> has_kids; available_range cap \<noteq> cap_objects cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 s cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B24 s cap\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace>
 3. \<And>s. \<lbrakk>uinv = Retype uref nt ts [dest_slot] False (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; obj_range \<subseteq> tot_free_range; free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* P) s; \<not> has_kids\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 s\<rbrace> liftE (get_cap uref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q23 s cap else (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace>
 4. \<And>s sa. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> (if has_kids then \<lambda>_. True else ?Q17 s) sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>uinv = Retype uref nt ts [dest_slot] has_kids (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; free_range \<subseteq> tot_free_range; \<not> has_kids \<longrightarrow> free_range = obj_range; cdl_current_domain s = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range free_range \<and>* P) s; s = sa\<rbrakk> \<Longrightarrow> (if has_kids then \<lambda>_. True else (\<lambda>sa. opt_cap uref sa \<noteq> None \<longrightarrow> (if available_range (the (opt_cap uref sa)) \<noteq> cap_objects (the (opt_cap uref sa)) then \<lambda>sb. \<forall>x\<in>{xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects (the (opt_cap uref sa)) \<and> available_range (the (opt_cap uref sa)) \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects (the (opt_cap uref sa))}. (?P'29 s (the (opt_cap uref sa)) () x and K (available_range (the (opt_cap uref sa)) = cap_objects (the (opt_cap uref sa)))) (detype (cap_objects (the (opt_cap uref sa))) sb) else (\<lambda>_. True)) sa)) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa y x. \<lbrakk>uinv = Retype uref nt ts [dest_slot] False (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; obj_range \<subseteq> tot_free_range; cdl_current_domain sa = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* P) sa; available_range y \<noteq> cap_objects y; \<not> has_kids; opt_cap uref sa = 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; free_range = obj_range\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>sa y x. \<lbrakk>uinv = Retype uref nt ts [dest_slot] False (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; obj_range \<subseteq> tot_free_range; cdl_current_domain sa = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* P) sa; available_range y \<noteq> cap_objects y; \<not> has_kids; opt_cap uref sa = 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; free_range = obj_range\<rbrakk> \<Longrightarrow> cdl.lift (uref \<mapsto>c ?cap67 sa y x \<and>* ?R67 sa y x) (?s67 sa y x)
 2. \<And>sa y x. \<lbrakk>uinv = Retype uref nt ts [dest_slot] False (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; obj_range \<subseteq> tot_free_range; cdl_current_domain sa = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* P) sa; available_range y \<noteq> cap_objects y; \<not> has_kids; opt_cap uref sa = 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; free_range = obj_range; \<exists>cap'. opt_cap uref (?s67 sa y x) = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid (?cap67 sa y x)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>sa y x. \<lbrakk>uinv = Retype uref nt ts [dest_slot] False (Suc 0); default_object nt ts minBound = Some obj; nt \<noteq> UntypedType; obj_range \<subseteq> tot_free_range; cdl_current_domain sa = minBound; cdl.lift (dest_slot \<mapsto>c NullCap \<and>* (SETSEPCONJ ptr:tot_free_range. ptr \<mapsto>o Untyped) \<and>* uref \<mapsto>c UntypedCap dev obj_range obj_range \<and>* P) sa; available_range y \<noteq> cap_objects y; \<not> has_kids; opt_cap uref sa = 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; free_range = obj_range; \<exists>cap'. opt_cap uref sa = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid (UntypedCap dev obj_range obj_range)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!