theory Retype_DP

lemma invoke_untyped_one_has_children:
  "uinv = (Retype uref nt ts [slot] has_kids (Suc 0))
  \<Longrightarrow> \<lbrace>K(nt \<noteq> UntypedType)\<rbrace> invoke_untyped uinv \<lbrace>\<lambda>r. has_children uref\<rbrace>,-" apply (simp add:invoke_untyped_def) apply (wp) apply (rule_tac P = "zip [slot] new_obj_refs \<noteq> []" in hoare_gen_asm) apply (rule hoare_strengthen_post[OF mapM_x_accumulate_checks]) apply (rule create_cap_has_children) apply wp apply simp apply (clarsimp simp:neq_Nil_conv) apply (cases slot, fastforce) apply wp+ apply (rule hoare_strengthen_post[OF generate_object_ids_rv]) apply clarsimp apply (wp unlessE_wp hoare_drop_imps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>K (nt \<noteq> UntypedType)\<rbrace> invoke_untyped uinv \<lbrace>\<lambda>r. has_children uref\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>\<lambda>y. nt \<noteq> UntypedType\<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 [slot] new_obj_refs)
od)
odE \<lbrace>\<lambda>r. has_children uref\<rbrace>, - proof (prove)
goal (7 subgoals):
 1. \<And>y untyped_cap new_obj_refs ya yb. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B8 y untyped_cap new_obj_refs ya yb\<rbrace> mapM_x (create_cap nt ts uref (untyped_is_device untyped_cap)) (zip [slot] new_obj_refs) \<lbrace>\<lambda>r. has_children uref\<rbrace>
 2. \<And>y untyped_cap new_obj_refs ya. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B7 y untyped_cap new_obj_refs ya\<rbrace> retype_region ts nt new_obj_refs \<lbrace>?B8 y untyped_cap new_obj_refs ya\<rbrace>
 3. \<And>y untyped_cap new_obj_refs. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B6 y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>?B7 y untyped_cap new_obj_refs\<rbrace>
 4. \<And>y untyped_cap. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B5 y untyped_cap\<rbrace> generate_object_ids (Suc 0) nt (available_range untyped_cap) \<lbrace>?B6 y untyped_cap\<rbrace>
 5. \<And>y. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B2 y\<rbrace> get_cap uref \<lbrace>?B5 y\<rbrace>
 6. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?P'1\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); nt \<noteq> UntypedType\<rbrakk> \<Longrightarrow> ?P'1 s proof (prove)
goal (7 subgoals):
 1. \<And>y untyped_cap new_obj_refs ya yb. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); zip [slot] new_obj_refs \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?P'9 y untyped_cap new_obj_refs ya yb\<rbrace> mapM_x (create_cap nt ts uref (untyped_is_device untyped_cap)) (zip [slot] new_obj_refs) \<lbrace>\<lambda>r. has_children uref\<rbrace>
 2. \<And>y untyped_cap new_obj_refs ya. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B7 y untyped_cap new_obj_refs ya\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>yb. ?P'9 y untyped_cap new_obj_refs ya yb and K (zip [slot] new_obj_refs \<noteq> [])\<rbrace>
 3. \<And>y untyped_cap new_obj_refs. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B6 y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>?B7 y untyped_cap new_obj_refs\<rbrace>
 4. \<And>y untyped_cap. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B5 y untyped_cap\<rbrace> generate_object_ids (Suc 0) nt (available_range untyped_cap) \<lbrace>?B6 y untyped_cap\<rbrace>
 5. \<And>y. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B2 y\<rbrace> get_cap uref \<lbrace>?B5 y\<rbrace>
 6. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?P'1\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); nt \<noteq> UntypedType\<rbrakk> \<Longrightarrow> ?P'1 s proof (prove)
goal (9 subgoals):
 1. \<And>y untyped_cap new_obj_refs ya yb x. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); zip [slot] new_obj_refs \<noteq> []; x \<in> set (zip [slot] new_obj_refs)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> create_cap nt ts uref (untyped_is_device untyped_cap) x \<lbrace>\<lambda>rv. ?P11 y untyped_cap new_obj_refs ya yb x\<rbrace>
 2. \<And>y untyped_cap new_obj_refs ya yb x yc. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); zip [slot] new_obj_refs \<noteq> []; x \<in> set (zip [slot] new_obj_refs); yc \<in> set (zip [slot] new_obj_refs)\<rbrakk> \<Longrightarrow> \<lbrace>?P11 y untyped_cap new_obj_refs ya yb yc\<rbrace> create_cap nt ts uref (untyped_is_device untyped_cap) x \<lbrace>\<lambda>rv. ?P11 y untyped_cap new_obj_refs ya yb yc\<rbrace>
 3. \<And>y untyped_cap new_obj_refs ya yb rv s. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); zip [slot] new_obj_refs \<noteq> []; \<forall>x\<in>set (zip [slot] new_obj_refs). ?P11 y untyped_cap new_obj_refs ya yb x s\<rbrakk> \<Longrightarrow> has_children uref s
 4. \<And>y untyped_cap new_obj_refs ya. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B7 y untyped_cap new_obj_refs ya\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>yb. (\<lambda>_. True) and K (zip [slot] new_obj_refs \<noteq> [])\<rbrace>
 5. \<And>y untyped_cap new_obj_refs. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B6 y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>?B7 y untyped_cap new_obj_refs\<rbrace>
 6. \<And>y untyped_cap. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B5 y untyped_cap\<rbrace> generate_object_ids (Suc 0) nt (available_range untyped_cap) \<lbrace>?B6 y untyped_cap\<rbrace>
 7. \<And>y. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B2 y\<rbrace> get_cap uref \<lbrace>?B5 y\<rbrace>
 8. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?P'1\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>s. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); nt \<noteq> UntypedType\<rbrakk> \<Longrightarrow> ?P'1 s proof (prove)
goal (8 subgoals):
 1. \<And>y untyped_cap new_obj_refs ya yb x yc. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); zip [slot] new_obj_refs \<noteq> []; x \<in> set (zip [slot] new_obj_refs); yc \<in> set (zip [slot] new_obj_refs)\<rbrakk> \<Longrightarrow> \<lbrace>has_children uref\<rbrace> create_cap nt ts uref (untyped_is_device untyped_cap) x \<lbrace>\<lambda>rv. has_children uref\<rbrace>
 2. \<And>y untyped_cap new_obj_refs ya yb rv s. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); zip [slot] new_obj_refs \<noteq> []; \<forall>x\<in>set (zip [slot] new_obj_refs). has_children uref s\<rbrakk> \<Longrightarrow> has_children uref s
 3. \<And>y untyped_cap new_obj_refs ya. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B7 y untyped_cap new_obj_refs ya\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>yb. (\<lambda>_. True) and K (zip [slot] new_obj_refs \<noteq> [])\<rbrace>
 4. \<And>y untyped_cap new_obj_refs. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B6 y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>?B7 y untyped_cap new_obj_refs\<rbrace>
 5. \<And>y untyped_cap. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B5 y untyped_cap\<rbrace> generate_object_ids (Suc 0) nt (available_range untyped_cap) \<lbrace>?B6 y untyped_cap\<rbrace>
 6. \<And>y. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B2 y\<rbrace> get_cap uref \<lbrace>?B5 y\<rbrace>
 7. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?P'1\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>s. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); nt \<noteq> UntypedType\<rbrakk> \<Longrightarrow> ?P'1 s proof (prove)
goal (7 subgoals):
 1. \<And>y untyped_cap new_obj_refs ya yb rv s. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); zip [slot] new_obj_refs \<noteq> []; \<forall>x\<in>set (zip [slot] new_obj_refs). has_children uref s\<rbrakk> \<Longrightarrow> has_children uref s
 2. \<And>y untyped_cap new_obj_refs ya. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B7 y untyped_cap new_obj_refs ya\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>yb. (\<lambda>_. True) and K (zip [slot] new_obj_refs \<noteq> [])\<rbrace>
 3. \<And>y untyped_cap new_obj_refs. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B6 y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>?B7 y untyped_cap new_obj_refs\<rbrace>
 4. \<And>y untyped_cap. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B5 y untyped_cap\<rbrace> generate_object_ids (Suc 0) nt (available_range untyped_cap) \<lbrace>?B6 y untyped_cap\<rbrace>
 5. \<And>y. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B2 y\<rbrace> get_cap uref \<lbrace>?B5 y\<rbrace>
 6. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?P'1\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); nt \<noteq> UntypedType\<rbrakk> \<Longrightarrow> ?P'1 s proof (prove)
goal (7 subgoals):
 1. \<And>new_obj_refs s. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); new_obj_refs \<noteq> []; (\<exists>a b ba. ((a, b), ba) \<in> set (zip [slot] new_obj_refs)) \<longrightarrow> has_children uref s\<rbrakk> \<Longrightarrow> has_children uref s
 2. \<And>y untyped_cap new_obj_refs ya. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B7 y untyped_cap new_obj_refs ya\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>yb. (\<lambda>_. True) and K (zip [slot] new_obj_refs \<noteq> [])\<rbrace>
 3. \<And>y untyped_cap new_obj_refs. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B6 y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>?B7 y untyped_cap new_obj_refs\<rbrace>
 4. \<And>y untyped_cap. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B5 y untyped_cap\<rbrace> generate_object_ids (Suc 0) nt (available_range untyped_cap) \<lbrace>?B6 y untyped_cap\<rbrace>
 5. \<And>y. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B2 y\<rbrace> get_cap uref \<lbrace>?B5 y\<rbrace>
 6. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?P'1\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); nt \<noteq> UntypedType\<rbrakk> \<Longrightarrow> ?P'1 s proof (prove)
goal (7 subgoals):
 1. \<And>s. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); \<forall>a b. (a, b) \<noteq> slot\<rbrakk> \<Longrightarrow> has_children uref s
 2. \<And>y untyped_cap new_obj_refs ya. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B7 y untyped_cap new_obj_refs ya\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>yb. (\<lambda>_. True) and K (zip [slot] new_obj_refs \<noteq> [])\<rbrace>
 3. \<And>y untyped_cap new_obj_refs. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B6 y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>?B7 y untyped_cap new_obj_refs\<rbrace>
 4. \<And>y untyped_cap. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B5 y untyped_cap\<rbrace> generate_object_ids (Suc 0) nt (available_range untyped_cap) \<lbrace>?B6 y untyped_cap\<rbrace>
 5. \<And>y. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B2 y\<rbrace> get_cap uref \<lbrace>?B5 y\<rbrace>
 6. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?P'1\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); nt \<noteq> UntypedType\<rbrakk> \<Longrightarrow> ?P'1 s proof (prove)
goal (6 subgoals):
 1. \<And>y untyped_cap new_obj_refs ya. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B7 y untyped_cap new_obj_refs ya\<rbrace> retype_region ts nt new_obj_refs \<lbrace>\<lambda>yb. (\<lambda>_. True) and K (zip [slot] new_obj_refs \<noteq> [])\<rbrace>
 2. \<And>y untyped_cap new_obj_refs. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B6 y untyped_cap new_obj_refs\<rbrace> update_available_range (available_range untyped_cap) (map pick new_obj_refs) uref untyped_cap \<lbrace>?B7 y untyped_cap new_obj_refs\<rbrace>
 3. \<And>y untyped_cap. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B5 y untyped_cap\<rbrace> generate_object_ids (Suc 0) nt (available_range untyped_cap) \<lbrace>?B6 y untyped_cap\<rbrace>
 4. \<And>y. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B2 y\<rbrace> get_cap uref \<lbrace>?B5 y\<rbrace>
 5. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?P'1\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); nt \<noteq> UntypedType\<rbrakk> \<Longrightarrow> ?P'1 s proof (prove)
goal (4 subgoals):
 1. \<And>y untyped_cap. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?P'43 y untyped_cap\<rbrace> generate_object_ids (Suc 0) nt (available_range untyped_cap) \<lbrace>\<lambda>rv. K (zip [slot] rv \<noteq> [])\<rbrace>
 2. \<And>y. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B2 y\<rbrace> get_cap uref \<lbrace>\<lambda>untyped_cap s. True \<and> ?P'43 y untyped_cap s\<rbrace>
 3. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?P'1\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); nt \<noteq> UntypedType\<rbrakk> \<Longrightarrow> ?P'1 s proof (prove)
goal (4 subgoals):
 1. \<And>y untyped_cap rv s. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); rv = map (\<lambda>x. {x}) (map pick rv) \<and> length rv = Suc 0 \<and> set (map pick rv) \<subseteq> available_range untyped_cap \<and> distinct (map pick rv)\<rbrakk> \<Longrightarrow> K (zip [slot] rv \<noteq> []) s
 2. \<And>y. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B2 y\<rbrace> get_cap uref \<lbrace>\<lambda>untyped_cap s. True \<and> K (nt \<noteq> UntypedType) s\<rbrace>
 3. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?P'1\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); nt \<noteq> UntypedType\<rbrakk> \<Longrightarrow> ?P'1 s proof (prove)
goal (3 subgoals):
 1. \<And>y. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?B2 y\<rbrace> get_cap uref \<lbrace>\<lambda>untyped_cap s. True \<and> K (nt \<noteq> UntypedType) s\<rbrace>
 2. uinv = Retype uref nt ts [slot] has_kids (Suc 0) \<Longrightarrow> \<lbrace>?P'1\<rbrace> unlessE has_kids (reset_untyped_cap uref) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. \<lbrakk>uinv = Retype uref nt ts [slot] has_kids (Suc 0); nt \<noteq> UntypedType\<rbrakk> \<Longrightarrow> ?P'1 s proof (prove)
goal:
No subgoals!