theory Untyped_DR

lemma create_caps_loop_dcorres:
  "dcorres dc \<top>
      (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)
            \<and> idle_thread s \<notin> fst ` fst ` set targets
            \<and> distinct (parent # map fst targets)
            \<and> (\<forall>tup \<in> set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s)
      (mapM_x
          (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz
                (transform_cslot_ptr parent) dev
                (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x)))
          targets)
      (mapM_x (Retype_A.create_cap type sz parent dev) targets)" apply (induct targets) apply (simp add: mapM_x_Nil) apply (clarsimp simp: mapM_x_Cons) apply (rule corres_guard_imp) apply (rule corres_split_nor) apply (rule create_cap_dcorres) apply assumption apply (wp create_cap_invs hoare_vcg_const_Ball_lift create_cap_mdb_cte_at[unfolded swp_def])+ apply simp apply (clarsimp simp: not_idle_thread_def swp_def) apply (auto simp: cte_wp_at_caps_of_state image_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> distinct (parent # map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets) proof (prove)
goal (2 subgoals):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set [] \<and> distinct (parent # map fst []) \<and> (\<forall>tup\<in>set []. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) []) (mapM_x (Retype_A.create_cap type sz parent dev) [])
 2. \<And>a targets. dcorres dc (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> distinct (parent # map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets) \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set (a # targets) \<and> distinct (parent # map fst (a # targets)) \<and> (\<forall>tup\<in>set (a # targets). cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) (a # targets)) (mapM_x (Retype_A.create_cap type sz parent dev) (a # targets)) proof (prove)
goal (1 subgoal):
 1. \<And>a targets. dcorres dc (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> distinct (parent # map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets) \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set (a # targets) \<and> distinct (parent # map fst (a # targets)) \<and> (\<forall>tup\<in>set (a # targets). cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) (a # targets)) (mapM_x (Retype_A.create_cap type sz parent dev) (a # targets)) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba targets. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets) \<Longrightarrow> dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<noteq> a \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<noteq> (a, b) \<and> parent \<notin> fst ` set targets \<and> (a, b) \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> cte_wp_at ((=) cap.NullCap) (a, b) s \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (do y <- Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (a, b), retype_transform_obj_ref type sz ba);
mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets
od) (do y <- Retype_A.create_cap type sz parent dev ((a, b), ba);
mapM_x (Retype_A.create_cap type sz parent dev) targets
od) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba targets. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets) \<Longrightarrow> dcorres (\<lambda>a b. True) (?Q16 a b ba targets) (?Q'16 a b ba targets) (do y <- Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (a, b), retype_transform_obj_ref type sz ba);
mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets
od) (do y <- Retype_A.create_cap type sz parent dev ((a, b), ba);
mapM_x (Retype_A.create_cap type sz parent dev) targets
od)
 2. \<And>a b ba targets s. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets); True\<rbrakk> \<Longrightarrow> ?Q16 a b ba targets s
 3. \<And>a b ba targets s. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets); cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<noteq> a \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<noteq> (a, b) \<and> parent \<notin> fst ` set targets \<and> (a, b) \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> cte_wp_at ((=) cap.NullCap) (a, b) s \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ?Q'16 a b ba targets s proof (prove)
goal (6 subgoals):
 1. \<And>a b ba targets. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets) \<Longrightarrow> dcorres dc (?P20 a b ba targets) (?P'20 a b ba targets) (Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (a, b), retype_transform_obj_ref type sz ba)) (Retype_A.create_cap type sz parent dev ((a, b), ba))
 2. \<And>a b ba targets. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets) \<Longrightarrow> dcorres (\<lambda>a b. True) (?R20 a b ba targets) (?R'20 a b ba targets) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets)
 3. \<And>a b ba targets. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets) \<Longrightarrow> \<lbrace>?Q20 a b ba targets\<rbrace> Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (a, b), retype_transform_obj_ref type sz ba) \<lbrace>\<lambda>x. ?R20 a b ba targets\<rbrace>
 4. \<And>a b ba targets. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets) \<Longrightarrow> \<lbrace>?Q'20 a b ba targets\<rbrace> Retype_A.create_cap type sz parent dev ((a, b), ba) \<lbrace>\<lambda>x. ?R'20 a b ba targets\<rbrace>
 5. \<And>a b ba targets s. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets); True\<rbrakk> \<Longrightarrow> (?P20 a b ba targets and ?Q20 a b ba targets) s
 6. \<And>a b ba targets s. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets); cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<noteq> a \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<noteq> (a, b) \<and> parent \<notin> fst ` set targets \<and> (a, b) \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> cte_wp_at ((=) cap.NullCap) (a, b) s \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (?P'20 a b ba targets and ?Q'20 a b ba targets) s proof (prove)
goal (5 subgoals):
 1. \<And>a b ba targets. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets) \<Longrightarrow> dcorres (\<lambda>a b. True) (?R20 a b ba targets) (?R'20 a b ba targets) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets)
 2. \<And>a b ba targets. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets) \<Longrightarrow> \<lbrace>?Q20 a b ba targets\<rbrace> Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (a, b), retype_transform_obj_ref type sz ba) \<lbrace>\<lambda>x. ?R20 a b ba targets\<rbrace>
 3. \<And>a b ba targets. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets) \<Longrightarrow> \<lbrace>?Q'20 a b ba targets\<rbrace> Retype_A.create_cap type sz parent dev ((a, b), ba) \<lbrace>\<lambda>x. ?R'20 a b ba targets\<rbrace>
 4. \<And>a b ba targets s. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q20 a b ba targets) s
 5. \<And>a b ba targets s. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets); cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<noteq> a \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<noteq> (a, b) \<and> parent \<notin> fst ` set targets \<and> (a, b) \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> cte_wp_at ((=) cap.NullCap) (a, b) s \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) (a, b) and not_idle_thread (fst (a, b)) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and ?Q'20 a b ba targets) s proof (prove)
goal (4 subgoals):
 1. \<And>a b ba targets. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets) \<Longrightarrow> \<lbrace>?Q20 a b ba targets\<rbrace> Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (a, b), retype_transform_obj_ref type sz ba) \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>a b ba targets. dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets) \<Longrightarrow> \<lbrace>?Q'20 a b ba targets\<rbrace> Retype_A.create_cap type sz parent dev ((a, b), ba) \<lbrace>\<lambda>x s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s\<rbrace>
 3. \<And>a b ba targets s. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q20 a b ba targets) s
 4. \<And>a b ba targets s. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets); cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<noteq> a \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<noteq> (a, b) \<and> parent \<notin> fst ` set targets \<and> (a, b) \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> cte_wp_at ((=) cap.NullCap) (a, b) s \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) (a, b) and not_idle_thread (fst (a, b)) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and ?Q'20 a b ba targets) s proof (prove)
goal (2 subgoals):
 1. \<And>a b ba targets s. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s
 2. \<And>a b ba targets s. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets); cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<noteq> a \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<noteq> (a, b) \<and> parent \<notin> fst ` set targets \<and> (a, b) \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> cte_wp_at ((=) cap.NullCap) (a, b) s \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) (a, b) and not_idle_thread (fst (a, b)) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and (\<lambda>s. (cte_wp_at ((\<noteq>) cap.NullCap) parent and K (parent \<noteq> (a, b))) s \<and> valid_idle s \<and> (mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) cap.NullCap) y s) (cdt s) \<and> cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> cte_wp_at (\<lambda>_. True) (fst ((a, b), ba)) s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>x\<in>set targets. (cte_wp_at ((=) cap.NullCap) (fst x) and K (fst x \<noteq> (a, b))) s) \<and> valid_etcbs s)) s proof (prove)
goal (1 subgoal):
 1. \<And>a b ba targets s. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets); cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<noteq> a \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<noteq> (a, b) \<and> parent \<notin> fst ` set targets \<and> (a, b) \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> cte_wp_at ((=) cap.NullCap) (a, b) s \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) (a, b) and not_idle_thread (fst (a, b)) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and (\<lambda>s. (cte_wp_at ((\<noteq>) cap.NullCap) parent and K (parent \<noteq> (a, b))) s \<and> valid_idle s \<and> (mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) cap.NullCap) y s) (cdt s) \<and> cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> cte_wp_at (\<lambda>_. True) (fst ((a, b), ba)) s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> parent \<notin> fst ` set targets \<and> distinct (map fst targets) \<and> (\<forall>x\<in>set targets. (cte_wp_at ((=) cap.NullCap) (fst x) and K (fst x \<noteq> (a, b))) s) \<and> valid_etcbs s)) s proof (prove)
goal (1 subgoal):
 1. \<And>a b targets s. \<lbrakk>dcorres (\<lambda>a b. True) (\<lambda>_. True) (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s) \<and> idle_thread s \<notin> fst ` fst ` set targets \<and> (\<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) (mapM_x (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) targets) (mapM_x (Retype_A.create_cap type sz parent dev) targets); cte_wp_at ((\<noteq>) cap.NullCap) parent s; valid_idle s; mdb_cte_at (\<lambda>a. cte_wp_at ((\<noteq>) cap.NullCap) a s) (cdt s); idle_thread s \<noteq> a; idle_thread s \<notin> fst ` fst ` set targets; parent \<noteq> (a, b); parent \<notin> fst ` set targets; (a, b) \<notin> fst ` set targets; distinct (map fst targets); cte_wp_at ((=) cap.NullCap) (a, b) s; \<forall>tup\<in>set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s; valid_etcbs s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) parent s \<and> cte_wp_at (\<lambda>_. True) (a, b) s \<and> (\<forall>x\<in>set targets. fst x \<noteq> (a, b)) proof (prove)
goal:
No subgoals!