theory Retype_DP

lemma invoke_untyped_cdt_inc[wp]:
  "\<lbrace>\<lambda>s. cdl_cdt s child = Some parent \<rbrace>
  invoke_untyped uinv
  \<lbrace>\<lambda>_ s. cdl_cdt s child = Some parent \<rbrace>" apply (clarsimp simp:invoke_untyped_def) apply (case_tac uinv) apply simp apply (rule hoare_pre) apply (wp unlessE_wp) apply clarsimp apply (wp mapM_x_wp[OF _ subset_refl]) apply (simp add:create_cap_def) apply (rule hoare_pre) apply (wp set_parent_other unless_wp unlessE_wp
               | wpc | simp)+ apply (simp add: reset_untyped_cap_def validE_def sum.case_eq_if) apply (rule_tac Q = "\<lambda>r s. cdl_cdt s child = Some parent" in hoare_post_imp) apply simp apply (wp whenE_wp mapME_x_inv_wp | simp)+ apply (clarsimp simp:detype_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl_cdt s child = Some parent\<rbrace> invoke_untyped uinv \<lbrace>\<lambda>_ s. cdl_cdt s child = Some parent\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl_cdt s child = Some parent\<rbrace> case uinv of Retype untyped_ref new_type type_size target_slots has_kids num_objects \<Rightarrow> doE unlessE has_kids $ reset_untyped_cap untyped_ref;
liftE $ do untyped_cap <- get_cap untyped_ref;
new_range <- return $ available_range untyped_cap;
new_obj_refs <- generate_object_ids num_objects new_type new_range;
update_available_range new_range (map pick new_obj_refs) untyped_ref untyped_cap;
retype_region type_size new_type new_obj_refs;
mapM_x (create_cap new_type type_size untyped_ref (untyped_is_device untyped_cap)) (zip target_slots new_obj_refs);
return ()
od
odE \<lbrace>\<lambda>_ s. cdl_cdt s child = Some parent\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>\<lambda>s. cdl_cdt s child = Some parent\<rbrace> case uinv of Retype untyped_ref new_type type_size target_slots has_kids num_objects \<Rightarrow> doE unlessE has_kids $ reset_untyped_cap untyped_ref;
liftE $ do untyped_cap <- get_cap untyped_ref;
new_range <- return $ available_range untyped_cap;
new_obj_refs <- generate_object_ids num_objects new_type new_range;
update_available_range new_range (map pick new_obj_refs) untyped_ref untyped_cap;
retype_region type_size new_type new_obj_refs;
mapM_x (create_cap new_type type_size untyped_ref (untyped_is_device untyped_cap)) (zip target_slots new_obj_refs);
return ()
od
odE \<lbrace>\<lambda>_ s. cdl_cdt s child = Some parent\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>\<lambda>s. cdl_cdt s child = Some parent\<rbrace> doE y <- unlessE x5 (reset_untyped_cap x1);
liftE (do untyped_cap <- get_cap x1;
new_obj_refs <- generate_object_ids x6 x2 (available_range untyped_cap);
y <- update_available_range (available_range untyped_cap) (map pick new_obj_refs) x1 untyped_cap;
y <- retype_region x3 x2 new_obj_refs;
mapM_x (create_cap x2 x3 x1 (untyped_is_device untyped_cap)) (zip x4 new_obj_refs)
od)
odE \<lbrace>\<lambda>_ s. cdl_cdt s child = Some parent\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 x5 x6. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?Q2 x1 x2 x3 x4 x5 x6\<rbrace> doE y <- unlessE x5 (reset_untyped_cap x1);
liftE (do untyped_cap <- get_cap x1;
new_obj_refs <- generate_object_ids x6 x2 (available_range untyped_cap);
y <- update_available_range (available_range untyped_cap) (map pick new_obj_refs) x1 untyped_cap;
y <- retype_region x3 x2 new_obj_refs;
mapM_x (create_cap x2 x3 x1 (untyped_is_device untyped_cap)) (zip x4 new_obj_refs)
od)
odE \<lbrace>\<lambda>_ s. cdl_cdt s child = Some parent\<rbrace>
 2. \<And>x1 x2 x3 x4 x5 x6 s. \<lbrakk>uinv = Retype x1 x2 x3 x4 x5 x6; cdl_cdt s child = Some parent\<rbrakk> \<Longrightarrow> ?Q2 x1 x2 x3 x4 x5 x6 s proof (prove)
goal (7 subgoals):
 1. \<And>x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs ya yb. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B12 x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs ya yb\<rbrace> mapM_x (create_cap x2 x3 x1 (untyped_is_device untyped_cap)) (zip x4 new_obj_refs) \<lbrace>\<lambda>_ s. cdl_cdt s child = Some parent\<rbrace>
 2. \<And>x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs ya. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B11 x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs ya\<rbrace> retype_region x3 x2 new_obj_refs \<lbrace>?B12 x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs ya\<rbrace>
 3. \<And>x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B10 x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) x1 untyped_cap \<lbrace>?B11 x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs\<rbrace>
 4. \<And>x1 x2 x3 x4 x5 x6 y untyped_cap. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B9 x1 x2 x3 x4 x5 x6 y untyped_cap\<rbrace> generate_object_ids x6 x2 (available_range untyped_cap) \<lbrace>?B10 x1 x2 x3 x4 x5 x6 y untyped_cap\<rbrace>
 5. \<And>x1 x2 x3 x4 x5 x6 y. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B7 x1 x2 x3 x4 x5 x6 y\<rbrace> get_cap x1 \<lbrace>?B9 x1 x2 x3 x4 x5 x6 y\<rbrace>
 6. \<And>x1 x2 x3 x4 x5 x6. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?Q2 x1 x2 x3 x4 x5 x6\<rbrace> unlessE x5 (reset_untyped_cap x1) \<lbrace>?B7 x1 x2 x3 x4 x5 x6\<rbrace>, \<lbrace>\<lambda>_ s. cdl_cdt s child = Some parent\<rbrace>
 7. \<And>x1 x2 x3 x4 x5 x6 s. \<lbrakk>uinv = Retype x1 x2 x3 x4 x5 x6; cdl_cdt s child = Some parent\<rbrakk> \<Longrightarrow> ?Q2 x1 x2 x3 x4 x5 x6 s proof (prove)
goal (7 subgoals):
 1. \<And>a b x2 x3 x4 x5 x6 untyped_cap new_obj_refs yb. uinv = Retype (a, b) x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B12 (a, b) x2 x3 x4 x5 x6 () untyped_cap new_obj_refs () yb\<rbrace> mapM_x (create_cap x2 x3 (a, b) (untyped_is_device untyped_cap)) (zip x4 new_obj_refs) \<lbrace>\<lambda>_ s. cdl_cdt s child = Some parent\<rbrace>
 2. \<And>x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs ya. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B11 x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs ya\<rbrace> retype_region x3 x2 new_obj_refs \<lbrace>?B12 x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs ya\<rbrace>
 3. \<And>x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B10 x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) x1 untyped_cap \<lbrace>?B11 x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs\<rbrace>
 4. \<And>x1 x2 x3 x4 x5 x6 y untyped_cap. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B9 x1 x2 x3 x4 x5 x6 y untyped_cap\<rbrace> generate_object_ids x6 x2 (available_range untyped_cap) \<lbrace>?B10 x1 x2 x3 x4 x5 x6 y untyped_cap\<rbrace>
 5. \<And>x1 x2 x3 x4 x5 x6 y. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B7 x1 x2 x3 x4 x5 x6 y\<rbrace> get_cap x1 \<lbrace>?B9 x1 x2 x3 x4 x5 x6 y\<rbrace>
 6. \<And>x1 x2 x3 x4 x5 x6. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?Q2 x1 x2 x3 x4 x5 x6\<rbrace> unlessE x5 (reset_untyped_cap x1) \<lbrace>?B7 x1 x2 x3 x4 x5 x6\<rbrace>, \<lbrace>\<lambda>_ s. cdl_cdt s child = Some parent\<rbrace>
 7. \<And>x1 x2 x3 x4 x5 x6 s. \<lbrakk>uinv = Retype x1 x2 x3 x4 x5 x6; cdl_cdt s child = Some parent\<rbrakk> \<Longrightarrow> ?Q2 x1 x2 x3 x4 x5 x6 s proof (prove)
goal (7 subgoals):
 1. \<And>a b x2 x3 x4 x5 x6 untyped_cap new_obj_refs yb x. \<lbrakk>uinv = Retype (a, b) x2 x3 x4 x5 x6; x \<in> set (zip x4 new_obj_refs)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. cdl_cdt a child = Some parent\<rbrace> create_cap x2 x3 (a, b) (untyped_is_device untyped_cap) x \<lbrace>\<lambda>_ a. cdl_cdt a child = Some parent\<rbrace>
 2. \<And>x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs ya. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B11 x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs ya\<rbrace> retype_region x3 x2 new_obj_refs \<lbrace>\<lambda>x11 x12. cdl_cdt x12 child = Some parent\<rbrace>
 3. \<And>x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B10 x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) x1 untyped_cap \<lbrace>?B11 x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs\<rbrace>
 4. \<And>x1 x2 x3 x4 x5 x6 y untyped_cap. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B9 x1 x2 x3 x4 x5 x6 y untyped_cap\<rbrace> generate_object_ids x6 x2 (available_range untyped_cap) \<lbrace>?B10 x1 x2 x3 x4 x5 x6 y untyped_cap\<rbrace>
 5. \<And>x1 x2 x3 x4 x5 x6 y. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B7 x1 x2 x3 x4 x5 x6 y\<rbrace> get_cap x1 \<lbrace>?B9 x1 x2 x3 x4 x5 x6 y\<rbrace>
 6. \<And>x1 x2 x3 x4 x5 x6. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?Q2 x1 x2 x3 x4 x5 x6\<rbrace> unlessE x5 (reset_untyped_cap x1) \<lbrace>?B7 x1 x2 x3 x4 x5 x6\<rbrace>, \<lbrace>\<lambda>_ s. cdl_cdt s child = Some parent\<rbrace>
 7. \<And>x1 x2 x3 x4 x5 x6 s. \<lbrakk>uinv = Retype x1 x2 x3 x4 x5 x6; cdl_cdt s child = Some parent\<rbrakk> \<Longrightarrow> ?Q2 x1 x2 x3 x4 x5 x6 s proof (prove)
goal (7 subgoals):
 1. \<And>a b x2 x3 x4 x5 x6 untyped_cap new_obj_refs x. \<lbrakk>uinv = Retype (a, b) x2 x3 x4 x5 x6; x \<in> set (zip x4 new_obj_refs)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. cdl_cdt a child = Some parent\<rbrace> case x of (dest_slot, obj_refs) \<Rightarrow> do old_cap <- get_cap dest_slot;
y <- assert (old_cap = NullCap);
y <- set_cap dest_slot (default_cap x2 obj_refs x3 (untyped_is_device untyped_cap));
set_parent dest_slot (a, b)
od \<lbrace>\<lambda>_ a. cdl_cdt a child = Some parent\<rbrace>
 2. \<And>x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs ya. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B11 x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs ya\<rbrace> retype_region x3 x2 new_obj_refs \<lbrace>\<lambda>x11 x12. cdl_cdt x12 child = Some parent\<rbrace>
 3. \<And>x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B10 x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) x1 untyped_cap \<lbrace>?B11 x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs\<rbrace>
 4. \<And>x1 x2 x3 x4 x5 x6 y untyped_cap. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B9 x1 x2 x3 x4 x5 x6 y untyped_cap\<rbrace> generate_object_ids x6 x2 (available_range untyped_cap) \<lbrace>?B10 x1 x2 x3 x4 x5 x6 y untyped_cap\<rbrace>
 5. \<And>x1 x2 x3 x4 x5 x6 y. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B7 x1 x2 x3 x4 x5 x6 y\<rbrace> get_cap x1 \<lbrace>?B9 x1 x2 x3 x4 x5 x6 y\<rbrace>
 6. \<And>x1 x2 x3 x4 x5 x6. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?Q2 x1 x2 x3 x4 x5 x6\<rbrace> unlessE x5 (reset_untyped_cap x1) \<lbrace>?B7 x1 x2 x3 x4 x5 x6\<rbrace>, \<lbrace>\<lambda>_ s. cdl_cdt s child = Some parent\<rbrace>
 7. \<And>x1 x2 x3 x4 x5 x6 s. \<lbrakk>uinv = Retype x1 x2 x3 x4 x5 x6; cdl_cdt s child = Some parent\<rbrakk> \<Longrightarrow> ?Q2 x1 x2 x3 x4 x5 x6 s proof (prove)
goal (8 subgoals):
 1. \<And>a b x2 x3 x4 x5 x6 untyped_cap new_obj_refs x. \<lbrakk>uinv = Retype (a, b) x2 x3 x4 x5 x6; x \<in> set (zip x4 new_obj_refs)\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 a b x2 x3 x4 x5 x6 untyped_cap new_obj_refs x\<rbrace> case x of (dest_slot, obj_refs) \<Rightarrow> do old_cap <- get_cap dest_slot;
y <- assert (old_cap = NullCap);
y <- set_cap dest_slot (default_cap x2 obj_refs x3 (untyped_is_device untyped_cap));
set_parent dest_slot (a, b)
od \<lbrace>\<lambda>_ a. cdl_cdt a child = Some parent\<rbrace>
 2. \<And>a b x2 x3 x4 x5 x6 untyped_cap new_obj_refs x s. \<lbrakk>uinv = Retype (a, b) x2 x3 x4 x5 x6; x \<in> set (zip x4 new_obj_refs); cdl_cdt s child = Some parent\<rbrakk> \<Longrightarrow> ?Q23 a b x2 x3 x4 x5 x6 untyped_cap new_obj_refs x s
 3. \<And>x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs ya. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B11 x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs ya\<rbrace> retype_region x3 x2 new_obj_refs \<lbrace>\<lambda>x11 x12. cdl_cdt x12 child = Some parent\<rbrace>
 4. \<And>x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B10 x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) x1 untyped_cap \<lbrace>?B11 x1 x2 x3 x4 x5 x6 y untyped_cap new_obj_refs\<rbrace>
 5. \<And>x1 x2 x3 x4 x5 x6 y untyped_cap. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B9 x1 x2 x3 x4 x5 x6 y untyped_cap\<rbrace> generate_object_ids x6 x2 (available_range untyped_cap) \<lbrace>?B10 x1 x2 x3 x4 x5 x6 y untyped_cap\<rbrace>
 6. \<And>x1 x2 x3 x4 x5 x6 y. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?B7 x1 x2 x3 x4 x5 x6 y\<rbrace> get_cap x1 \<lbrace>?B9 x1 x2 x3 x4 x5 x6 y\<rbrace>
 7. \<And>x1 x2 x3 x4 x5 x6. uinv = Retype x1 x2 x3 x4 x5 x6 \<Longrightarrow> \<lbrace>?Q2 x1 x2 x3 x4 x5 x6\<rbrace> unlessE x5 (reset_untyped_cap x1) \<lbrace>?B7 x1 x2 x3 x4 x5 x6\<rbrace>, \<lbrace>\<lambda>_ s. cdl_cdt s child = Some parent\<rbrace>
 8. \<And>x1 x2 x3 x4 x5 x6 s. \<lbrakk>uinv = Retype x1 x2 x3 x4 x5 x6; cdl_cdt s child = Some parent\<rbrakk> \<Longrightarrow> ?Q2 x1 x2 x3 x4 x5 x6 s proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 x5 x6. \<lbrakk>uinv = Retype x1 x2 x3 x4 False x6; \<not> x5\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 x1 x2 x3 x4 False x6\<rbrace> reset_untyped_cap x1 \<lbrace>\<lambda>y s. (\<exists>y. opt_cap x1 s = Some y) \<longrightarrow> cdl_cdt s child = Some parent\<rbrace>, \<lbrace>\<lambda>_ s. cdl_cdt s child = Some parent\<rbrace>
 2. \<And>x1 x2 x3 x4 x5 x6 s. \<lbrakk>uinv = Retype x1 x2 x3 x4 x5 x6; cdl_cdt s child = Some parent\<rbrakk> \<Longrightarrow> (if x5 then \<lambda>s. opt_cap x1 s \<noteq> None \<longrightarrow> cdl_cdt s child = Some parent else ?Q59 x1 x2 x3 x4 x5 x6) s proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 x5 x6. \<lbrakk>uinv = Retype x1 x2 x3 x4 False x6; \<not> x5\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 x1 x2 x3 x4 False x6\<rbrace> doE cap <- liftE (get_cap x1);
whenE (available_range cap \<noteq> cap_objects cap) (doE y <- liftE (modify (detype (cap_objects cap)));
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}) >>=E mapME_x (\<lambda>r. doE y <- liftE (set_cap x1 (set_available_range cap r));
returnOk () \<sqinter> throw
odE)
odE)
odE \<lbrace>\<lambda>v s. (isLeft v \<longrightarrow> cdl_cdt s child = Some parent) \<and> (isRight v \<longrightarrow> (\<exists>y. opt_cap x1 s = Some y) \<longrightarrow> cdl_cdt s child = Some parent)\<rbrace>
 2. \<And>x1 x2 x3 x4 x5 x6 s. \<lbrakk>uinv = Retype x1 x2 x3 x4 x5 x6; cdl_cdt s child = Some parent\<rbrakk> \<Longrightarrow> (if x5 then \<lambda>s. opt_cap x1 s \<noteq> None \<longrightarrow> cdl_cdt s child = Some parent else ?Q59 x1 x2 x3 x4 x5 x6) s proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2 x3 x4 x5 x6 rv s. \<lbrakk>uinv = Retype x1 x2 x3 x4 False x6; \<not> x5; cdl_cdt s child = Some parent\<rbrakk> \<Longrightarrow> (isLeft rv \<longrightarrow> cdl_cdt s child = Some parent) \<and> (isRight rv \<longrightarrow> (\<exists>y. opt_cap x1 s = Some y) \<longrightarrow> cdl_cdt s child = Some parent)
 2. \<And>x1 x2 x3 x4 x5 x6. \<lbrakk>uinv = Retype x1 x2 x3 x4 False x6; \<not> x5\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 x1 x2 x3 x4 False x6\<rbrace> doE cap <- liftE (get_cap x1);
whenE (available_range cap \<noteq> cap_objects cap) (doE y <- liftE (modify (detype (cap_objects cap)));
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}) >>=E mapME_x (\<lambda>r. doE y <- liftE (set_cap x1 (set_available_range cap r));
returnOk () \<sqinter> throw
odE)
odE)
odE \<lbrace>\<lambda>r s. cdl_cdt s child = Some parent\<rbrace>
 3. \<And>x1 x2 x3 x4 x5 x6 s. \<lbrakk>uinv = Retype x1 x2 x3 x4 x5 x6; cdl_cdt s child = Some parent\<rbrakk> \<Longrightarrow> (if x5 then \<lambda>s. opt_cap x1 s \<noteq> None \<longrightarrow> cdl_cdt s child = Some parent else ?Q59 x1 x2 x3 x4 x5 x6) s proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 x5 x6. \<lbrakk>uinv = Retype x1 x2 x3 x4 False x6; \<not> x5\<rbrakk> \<Longrightarrow> \<lbrace>?Q59 x1 x2 x3 x4 False x6\<rbrace> doE cap <- liftE (get_cap x1);
whenE (available_range cap \<noteq> cap_objects cap) (doE y <- liftE (modify (detype (cap_objects cap)));
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}) >>=E mapME_x (\<lambda>r. doE y <- liftE (set_cap x1 (set_available_range cap r));
returnOk () \<sqinter> throw
odE)
odE)
odE \<lbrace>\<lambda>r s. cdl_cdt s child = Some parent\<rbrace>
 2. \<And>x1 x2 x3 x4 x5 x6 s. \<lbrakk>uinv = Retype x1 x2 x3 x4 x5 x6; cdl_cdt s child = Some parent\<rbrakk> \<Longrightarrow> (if x5 then \<lambda>s. opt_cap x1 s \<noteq> None \<longrightarrow> cdl_cdt s child = Some parent else ?Q59 x1 x2 x3 x4 x5 x6) s proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 s. \<lbrakk>uinv = Retype x1 x2 x3 x4 x5 x6; cdl_cdt s child = Some parent\<rbrakk> \<Longrightarrow> available_range (the (opt_cap x1 s)) \<noteq> cap_objects (the (opt_cap x1 s)) \<longrightarrow> \<not> x5 \<longrightarrow> (\<exists>y. opt_cap x1 s = Some y) \<longrightarrow> (\<exists>x. (\<forall>S\<in>set x. S \<subseteq> cap_objects (the (opt_cap x1 s)) \<and> available_range (the (opt_cap x1 s)) \<subset> S) \<and> x \<noteq> [] \<and> last x = cap_objects (the (opt_cap x1 s))) \<longrightarrow> cdl_cdt (detype (cap_objects (the (opt_cap x1 s))) s) child = Some parent proof (prove)
goal:
No subgoals!