theory Untyped_DR

lemma create_cap_dcorres:
  "dcorres dc \<top> (cte_at parent and cte_wp_at ((=) cap.NullCap) slot
                       and not_idle_thread (fst slot) and valid_idle and valid_etcbs
                       and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)))
        (Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev
                 (transform_cslot_ptr slot, retype_transform_obj_ref type sz ptr))
        (Retype_A.create_cap type sz parent dev (slot, ptr))" supply if_cong[cong] apply (simp add: Untyped_D.create_cap_def Retype_A.create_cap_def) apply (rule stronger_corres_guard_imp) apply (rule corres_gets_the_bind) apply (rule corres_underlying_gets_pre_lhs) apply (rule corres_assert_lhs) apply (simp add: set_cap_set_parent_swap bind_assoc[symmetric]) apply (rule corres_split_nor) apply (simp add: bind_assoc set_original_def create_cap_ext_def
                        set_cdt_modify gets_fold_into_modify update_cdt_list_def
                        modify_modify set_cdt_list_modify) apply (rule dcorres_set_parent_helper) apply (rule_tac P'="\<lambda>s. mdb_cte_at (swp cte_at s) (cdt s)
                                \<and> cte_at parent s \<and> cte_at slot s"
                      in corres_modify[where P=\<top>]) apply (clarsimp simp: transform_def transform_current_thread_def
                             transform_asid_table_def transform_objects_def) apply (simp add: transform_cdt_def fun_upd_def[symmetric]) apply (subst map_lift_over_upd) apply (rule_tac P=\<top> and s=s' in transform_cdt_slot_inj_on_cte_at) apply (auto dest: mdb_cte_atD[rotated] elim!: ranE)[1] apply simp apply (fold dc_def) apply (rule set_cap_corres, simp_all add: transform_default_cap)[1] apply (wp|simp)+ apply (clarsimp simp: cte_wp_at_caps_of_state caps_of_state_transform_opt_cap not_idle_thread_def) apply (clarsimp simp: swp_def not_idle_thread_def cte_wp_at_caps_of_state) apply (drule mdb_cte_at_cdt_null) apply (clarsimp simp:cte_wp_at_caps_of_state swp_def) apply (fastforce simp:mdb_cte_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) (Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr slot, retype_transform_obj_ref type sz ptr)) (Retype_A.create_cap type sz parent dev (slot, ptr)) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) (Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev (transform_cslot_ptr slot, retype_transform_obj_ref type sz ptr)) (Retype_A.create_cap type sz parent dev (slot, ptr)) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) (do old_cap <- KHeap_D.get_cap (transform_cslot_ptr slot);
y <- assert (old_cap = cdl_cap.NullCap);
y <- KHeap_D.set_cap (transform_cslot_ptr slot) (Types_D.default_cap (translate_object_type type) (retype_transform_obj_ref type sz ptr) sz dev);
set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent)
od) (do dest_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
y <- set_cdt (cdt(slot \<mapsto> parent));
y <- create_cap_ext parent slot dest_p;
y <- set_original slot True;
CSpaceAcc_A.set_cap (Retype_A.default_cap type ptr sz dev) slot
od) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (do old_cap <- KHeap_D.get_cap (transform_cslot_ptr slot);
y <- assert (old_cap = cdl_cap.NullCap);
y <- KHeap_D.set_cap (transform_cslot_ptr slot) (Types_D.default_cap (translate_object_type type) (retype_transform_obj_ref type sz ptr) sz dev);
set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent)
od) (do dest_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
y <- set_cdt (cdt(slot \<mapsto> parent));
y <- create_cap_ext parent slot dest_p;
y <- set_original slot True;
CSpaceAcc_A.set_cap (Retype_A.default_cap type ptr sz dev) slot
od)
 2. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (3 subgoals):
 1. dcorres dc ?P4 ?Q' (do old_cap <- gets (the \<circ> opt_cap (transform_cslot_ptr slot));
y <- assert (old_cap = cdl_cap.NullCap);
y <- KHeap_D.set_cap (transform_cslot_ptr slot) (Types_D.default_cap (translate_object_type type) (retype_transform_obj_ref type sz ptr) sz dev);
set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent)
od) (do dest_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
y <- set_cdt (cdt(slot \<mapsto> parent));
y <- create_cap_ext parent slot dest_p;
y <- set_original slot True;
CSpaceAcc_A.set_cap (Retype_A.default_cap type ptr sz dev) slot
od)
 2. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (?P4 and (\<lambda>s. opt_cap (transform_cslot_ptr slot) s \<noteq> None)) s
 3. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (3 subgoals):
 1. \<And>old_cap. dcorres dc (?P6 old_cap) ?Q' (do y <- assert (old_cap = cdl_cap.NullCap);
y <- KHeap_D.set_cap (transform_cslot_ptr slot) (Types_D.default_cap (translate_object_type type) (retype_transform_obj_ref type sz ptr) sz dev);
set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent)
od) (do dest_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
y <- set_cdt (cdt(slot \<mapsto> parent));
y <- create_cap_ext parent slot dest_p;
y <- set_original slot True;
CSpaceAcc_A.set_cap (Retype_A.default_cap type ptr sz dev) slot
od)
 2. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. ?P6 ((the \<circ> opt_cap (transform_cslot_ptr slot)) s) s) and (\<lambda>s. opt_cap (transform_cslot_ptr slot) s \<noteq> None)) s
 3. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (3 subgoals):
 1. \<And>old_cap. old_cap = cdl_cap.NullCap \<Longrightarrow> dcorres dc (?P8 old_cap) ?Q' (do y <- KHeap_D.set_cap (transform_cslot_ptr slot) (Types_D.default_cap (translate_object_type type) (retype_transform_obj_ref type sz ptr) sz dev);
set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent)
od) (do dest_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
y <- set_cdt (cdt(slot \<mapsto> parent));
y <- create_cap_ext parent slot dest_p;
y <- set_original slot True;
CSpaceAcc_A.set_cap (Retype_A.default_cap type ptr sz dev) slot
od)
 2. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. (the \<circ> opt_cap (transform_cslot_ptr slot)) s = cdl_cap.NullCap \<and> ?P8 ((the \<circ> opt_cap (transform_cslot_ptr slot)) s) s) and (\<lambda>s. opt_cap (transform_cslot_ptr slot) s \<noteq> None)) s
 3. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (3 subgoals):
 1. dcorres (\<lambda>a b. True) (?P8 cdl_cap.NullCap) ?Q' (do y <- set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent);
KHeap_D.set_cap (transform_cslot_ptr slot) (Types_D.default_cap (translate_object_type type) (retype_transform_obj_ref type sz ptr) sz dev)
od) (do y <- do y <- do dest_p <- gets (\<lambda>s. cdt s slot);
y <- do cdt <- gets cdt;
set_cdt (cdt(slot \<mapsto> parent))
od;
create_cap_ext parent slot dest_p
od;
set_original slot True
od;
CSpaceAcc_A.set_cap (Retype_A.default_cap type ptr sz dev) slot
od)
 2. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. (the \<circ> opt_cap (transform_cslot_ptr slot)) s = cdl_cap.NullCap \<and> ?P8 ((the \<circ> opt_cap (transform_cslot_ptr slot)) s) s) and (\<lambda>s. opt_cap (transform_cslot_ptr slot) s \<noteq> None)) s
 3. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (6 subgoals):
 1. dcorres dc (?P15 cdl_cap.NullCap) ?P'10 (set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent)) (do y <- do dest_p <- gets (\<lambda>s. cdt s slot);
y <- do cdt <- gets cdt;
set_cdt (cdt(slot \<mapsto> parent))
od;
create_cap_ext parent slot dest_p
od;
set_original slot True
od)
 2. dcorres (\<lambda>a b. True) ?R10 ?R'10 (KHeap_D.set_cap (transform_cslot_ptr slot) (Types_D.default_cap (translate_object_type type) (retype_transform_obj_ref type sz ptr) sz dev)) (CSpaceAcc_A.set_cap (Retype_A.default_cap type ptr sz dev) slot)
 3. \<lbrace>?Q14 cdl_cap.NullCap\<rbrace> set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent) \<lbrace>\<lambda>x. ?R10\<rbrace>
 4. \<lbrace>?Q'10\<rbrace> do y <- do dest_p <- gets (\<lambda>s. cdt s slot);
y <- do cdt <- gets cdt;
set_cdt (cdt(slot \<mapsto> parent))
od;
create_cap_ext parent slot dest_p
od;
set_original slot True
od \<lbrace>\<lambda>x. ?R'10\<rbrace>
 5. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. (the \<circ> opt_cap (transform_cslot_ptr slot)) s = cdl_cap.NullCap \<and> (?P15 ((the \<circ> opt_cap (transform_cslot_ptr slot)) s) and ?Q14 ((the \<circ> opt_cap (transform_cslot_ptr slot)) s)) s) and (\<lambda>s. opt_cap (transform_cslot_ptr slot) s \<noteq> None)) s
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (?P'10 and ?Q'10) s' proof (prove)
goal (6 subgoals):
 1. dcorres dc (?P15 cdl_cap.NullCap) ?P'10 (set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent)) (modify ((\<lambda>s. s\<lparr>is_original_cap := (is_original_cap s)(slot := True)\<rparr>) \<circ> (\<lambda>s. s\<lparr>cdt_list := (case cdt s slot of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>) p) slot))(parent := slot # (case cdt s slot of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>) p) slot)) parent), cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>)))
 2. dcorres (\<lambda>a b. True) ?R10 ?R'10 (KHeap_D.set_cap (transform_cslot_ptr slot) (Types_D.default_cap (translate_object_type type) (retype_transform_obj_ref type sz ptr) sz dev)) (CSpaceAcc_A.set_cap (Retype_A.default_cap type ptr sz dev) slot)
 3. \<lbrace>?Q14 cdl_cap.NullCap\<rbrace> set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent) \<lbrace>\<lambda>x. ?R10\<rbrace>
 4. \<lbrace>?Q'10\<rbrace> do y <- do dest_p <- gets (\<lambda>s. cdt s slot);
y <- do cdt <- gets cdt;
set_cdt (cdt(slot \<mapsto> parent))
od;
create_cap_ext parent slot dest_p
od;
set_original slot True
od \<lbrace>\<lambda>x. ?R'10\<rbrace>
 5. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. (the \<circ> opt_cap (transform_cslot_ptr slot)) s = cdl_cap.NullCap \<and> (?P15 ((the \<circ> opt_cap (transform_cslot_ptr slot)) s) and ?Q14 ((the \<circ> opt_cap (transform_cslot_ptr slot)) s)) s) and (\<lambda>s. opt_cap (transform_cslot_ptr slot) s \<noteq> None)) s
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (?P'10 and ?Q'10) s' proof (prove)
goal (6 subgoals):
 1. dcorres dc (\<lambda>_. True) ?P20 (modify (\<lambda>s. s\<lparr>cdl_cdt := (cdl_cdt s)(transform_cslot_ptr slot \<mapsto> transform_cslot_ptr parent)\<rparr>)) (modify ((\<lambda>s. s\<lparr>is_original_cap := (is_original_cap s)(slot := True)\<rparr>) \<circ> (\<lambda>s. s\<lparr>cdt_list := (case cdt s slot of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>) p) slot))(parent := slot # (case cdt s slot of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>) p) slot)) parent), cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>)))
 2. dcorres (\<lambda>a b. True) ?R10 ?R'10 (KHeap_D.set_cap (transform_cslot_ptr slot) (Types_D.default_cap (translate_object_type type) (retype_transform_obj_ref type sz ptr) sz dev)) (CSpaceAcc_A.set_cap (Retype_A.default_cap type ptr sz dev) slot)
 3. \<lbrace>?Q14 cdl_cap.NullCap\<rbrace> set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent) \<lbrace>\<lambda>x. ?R10\<rbrace>
 4. \<lbrace>?Q'10\<rbrace> do y <- do dest_p <- gets (\<lambda>s. cdt s slot);
y <- do cdt <- gets cdt;
set_cdt (cdt(slot \<mapsto> parent))
od;
create_cap_ext parent slot dest_p
od;
set_original slot True
od \<lbrace>\<lambda>x. ?R'10\<rbrace>
 5. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. (the \<circ> opt_cap (transform_cslot_ptr slot)) s = cdl_cap.NullCap \<and> ((\<lambda>a. True) and ?Q14 ((the \<circ> opt_cap (transform_cslot_ptr slot)) s)) s) and (\<lambda>s. opt_cap (transform_cslot_ptr slot) s \<noteq> None)) s
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdt s slot = None \<and> cte_wp_at (\<lambda>_. True) slot s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> ?P20 s) and ?Q'10) s' proof (prove)
goal (6 subgoals):
 1. \<And>s s'. \<lbrakk>True; mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s') \<and> cte_wp_at (\<lambda>_. True) parent s' \<and> cte_wp_at (\<lambda>_. True) slot s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (s\<lparr>cdl_cdt := (cdl_cdt s)(transform_cslot_ptr slot \<mapsto> transform_cslot_ptr parent)\<rparr>, ((\<lambda>s. s\<lparr>is_original_cap := (is_original_cap s)(slot := True)\<rparr>) \<circ> (\<lambda>s. s\<lparr>cdt_list := (case cdt s slot of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>) p) slot))(parent := slot # (case cdt s slot of None \<Rightarrow> cdt_list (s\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>) | Some p \<Rightarrow> (cdt_list (s\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>))(p := list_remove (cdt_list (s\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>) p) slot)) parent), cdt := \<lambda>a. if a = slot then Some parent else cdt s a\<rparr>)) s') \<in> {ss'. transform (snd ss') = fst ss'}
 2. dcorres (\<lambda>a b. True) ?R10 ?R'10 (KHeap_D.set_cap (transform_cslot_ptr slot) (Types_D.default_cap (translate_object_type type) (retype_transform_obj_ref type sz ptr) sz dev)) (CSpaceAcc_A.set_cap (Retype_A.default_cap type ptr sz dev) slot)
 3. \<lbrace>?Q14 cdl_cap.NullCap\<rbrace> set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent) \<lbrace>\<lambda>x. ?R10\<rbrace>
 4. \<lbrace>?Q'10\<rbrace> do y <- do dest_p <- gets (\<lambda>s. cdt s slot);
y <- do cdt <- gets cdt;
set_cdt (cdt(slot \<mapsto> parent))
od;
create_cap_ext parent slot dest_p
od;
set_original slot True
od \<lbrace>\<lambda>x. ?R'10\<rbrace>
 5. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. (the \<circ> opt_cap (transform_cslot_ptr slot)) s = cdl_cap.NullCap \<and> ((\<lambda>a. True) and ?Q14 ((the \<circ> opt_cap (transform_cslot_ptr slot)) s)) s) and (\<lambda>s. opt_cap (transform_cslot_ptr slot) s \<noteq> None)) s
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdt s slot = None \<and> cte_wp_at (\<lambda>_. True) slot s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> cte_wp_at (\<lambda>_. True) slot s) and ?Q'10) s' proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); cte_wp_at (\<lambda>_. True) parent s'; cte_wp_at (\<lambda>_. True) slot s'\<rbrakk> \<Longrightarrow> transform_cdt (s'\<lparr>cdt_list := (case cdt s' slot of None \<Rightarrow> cdt_list (s'\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s' a\<rparr>) | Some p \<Rightarrow> (cdt_list (s'\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s' a\<rparr>))(p := list_remove (cdt_list (s'\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s' a\<rparr>) p) slot))(parent := slot # (case cdt s' slot of None \<Rightarrow> cdt_list (s'\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s' a\<rparr>) | Some p \<Rightarrow> (cdt_list (s'\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s' a\<rparr>))(p := list_remove (cdt_list (s'\<lparr>cdt := \<lambda>a. if a = slot then Some parent else cdt s' a\<rparr>) p) slot)) parent), cdt := \<lambda>a. if a = slot then Some parent else cdt s' a\<rparr>) = (transform_cdt s')(transform_cslot_ptr slot \<mapsto> transform_cslot_ptr parent)
 2. dcorres (\<lambda>a b. True) ?R10 ?R'10 (KHeap_D.set_cap (transform_cslot_ptr slot) (Types_D.default_cap (translate_object_type type) (retype_transform_obj_ref type sz ptr) sz dev)) (CSpaceAcc_A.set_cap (Retype_A.default_cap type ptr sz dev) slot)
 3. \<lbrace>?Q14 cdl_cap.NullCap\<rbrace> set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent) \<lbrace>\<lambda>x. ?R10\<rbrace>
 4. \<lbrace>?Q'10\<rbrace> do y <- do dest_p <- gets (\<lambda>s. cdt s slot);
y <- do cdt <- gets cdt;
set_cdt (cdt(slot \<mapsto> parent))
od;
create_cap_ext parent slot dest_p
od;
set_original slot True
od \<lbrace>\<lambda>x. ?R'10\<rbrace>
 5. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. (the \<circ> opt_cap (transform_cslot_ptr slot)) s = cdl_cap.NullCap \<and> ((\<lambda>a. True) and ?Q14 ((the \<circ> opt_cap (transform_cslot_ptr slot)) s)) s) and (\<lambda>s. opt_cap (transform_cslot_ptr slot) s \<noteq> None)) s
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdt s slot = None \<and> cte_wp_at (\<lambda>_. True) slot s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> cte_wp_at (\<lambda>_. True) slot s) and ?Q'10) s' proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); cte_wp_at (\<lambda>_. True) parent s'; cte_wp_at (\<lambda>_. True) slot s'\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr ((cdt s')(slot \<mapsto> parent)) = (map_lift_over transform_cslot_ptr (cdt s'))(transform_cslot_ptr slot \<mapsto> transform_cslot_ptr parent)
 2. dcorres (\<lambda>a b. True) ?R10 ?R'10 (KHeap_D.set_cap (transform_cslot_ptr slot) (Types_D.default_cap (translate_object_type type) (retype_transform_obj_ref type sz ptr) sz dev)) (CSpaceAcc_A.set_cap (Retype_A.default_cap type ptr sz dev) slot)
 3. \<lbrace>?Q14 cdl_cap.NullCap\<rbrace> set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent) \<lbrace>\<lambda>x. ?R10\<rbrace>
 4. \<lbrace>?Q'10\<rbrace> do y <- do dest_p <- gets (\<lambda>s. cdt s slot);
y <- do cdt <- gets cdt;
set_cdt (cdt(slot \<mapsto> parent))
od;
create_cap_ext parent slot dest_p
od;
set_original slot True
od \<lbrace>\<lambda>x. ?R'10\<rbrace>
 5. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. (the \<circ> opt_cap (transform_cslot_ptr slot)) s = cdl_cap.NullCap \<and> ((\<lambda>a. True) and ?Q14 ((the \<circ> opt_cap (transform_cslot_ptr slot)) s)) s) and (\<lambda>s. opt_cap (transform_cslot_ptr slot) s \<noteq> None)) s
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdt s slot = None \<and> cte_wp_at (\<lambda>_. True) slot s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> cte_wp_at (\<lambda>_. True) slot s) and ?Q'10) s' proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); cte_wp_at (\<lambda>_. True) parent s'; cte_wp_at (\<lambda>_. True) slot s'\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({slot} \<union> set_option (Some parent) \<union> dom (cdt s') \<union> ran (cdt s'))
 2. \<And>s'. \<lbrakk>mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); cte_wp_at (\<lambda>_. True) parent s'; cte_wp_at (\<lambda>_. True) slot s'\<rbrakk> \<Longrightarrow> (map_lift_over transform_cslot_ptr (cdt s'))(transform_cslot_ptr slot := map_option transform_cslot_ptr (Some parent)) = (map_lift_over transform_cslot_ptr (cdt s'))(transform_cslot_ptr slot \<mapsto> transform_cslot_ptr parent)
 3. dcorres (\<lambda>a b. True) ?R10 ?R'10 (KHeap_D.set_cap (transform_cslot_ptr slot) (Types_D.default_cap (translate_object_type type) (retype_transform_obj_ref type sz ptr) sz dev)) (CSpaceAcc_A.set_cap (Retype_A.default_cap type ptr sz dev) slot)
 4. \<lbrace>?Q14 cdl_cap.NullCap\<rbrace> set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent) \<lbrace>\<lambda>x. ?R10\<rbrace>
 5. \<lbrace>?Q'10\<rbrace> do y <- do dest_p <- gets (\<lambda>s. cdt s slot);
y <- do cdt <- gets cdt;
set_cdt (cdt(slot \<mapsto> parent))
od;
create_cap_ext parent slot dest_p
od;
set_original slot True
od \<lbrace>\<lambda>x. ?R'10\<rbrace>
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. (the \<circ> opt_cap (transform_cslot_ptr slot)) s = cdl_cap.NullCap \<and> ((\<lambda>a. True) and ?Q14 ((the \<circ> opt_cap (transform_cslot_ptr slot)) s)) s) and (\<lambda>s. opt_cap (transform_cslot_ptr slot) s \<noteq> None)) s
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdt s slot = None \<and> cte_wp_at (\<lambda>_. True) slot s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> cte_wp_at (\<lambda>_. True) slot s) and ?Q'10) s' proof (prove)
goal (7 subgoals):
 1. \<And>s' x. \<lbrakk>mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); cte_wp_at (\<lambda>_. True) parent s'; cte_wp_at (\<lambda>_. True) slot s'; x \<in> {slot} \<union> set_option (Some parent) \<union> dom (cdt s') \<union> ran (cdt s')\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) x s'
 2. \<And>s'. \<lbrakk>mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); cte_wp_at (\<lambda>_. True) parent s'; cte_wp_at (\<lambda>_. True) slot s'\<rbrakk> \<Longrightarrow> (map_lift_over transform_cslot_ptr (cdt s'))(transform_cslot_ptr slot := map_option transform_cslot_ptr (Some parent)) = (map_lift_over transform_cslot_ptr (cdt s'))(transform_cslot_ptr slot \<mapsto> transform_cslot_ptr parent)
 3. dcorres (\<lambda>a b. True) ?R10 ?R'10 (KHeap_D.set_cap (transform_cslot_ptr slot) (Types_D.default_cap (translate_object_type type) (retype_transform_obj_ref type sz ptr) sz dev)) (CSpaceAcc_A.set_cap (Retype_A.default_cap type ptr sz dev) slot)
 4. \<lbrace>?Q14 cdl_cap.NullCap\<rbrace> set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent) \<lbrace>\<lambda>x. ?R10\<rbrace>
 5. \<lbrace>?Q'10\<rbrace> do y <- do dest_p <- gets (\<lambda>s. cdt s slot);
y <- do cdt <- gets cdt;
set_cdt (cdt(slot \<mapsto> parent))
od;
create_cap_ext parent slot dest_p
od;
set_original slot True
od \<lbrace>\<lambda>x. ?R'10\<rbrace>
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. (the \<circ> opt_cap (transform_cslot_ptr slot)) s = cdl_cap.NullCap \<and> ((\<lambda>a. True) and ?Q14 ((the \<circ> opt_cap (transform_cslot_ptr slot)) s)) s) and (\<lambda>s. opt_cap (transform_cslot_ptr slot) s \<noteq> None)) s
 7. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdt s slot = None \<and> cte_wp_at (\<lambda>_. True) slot s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> cte_wp_at (\<lambda>_. True) slot s) and ?Q'10) s' proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s') (cdt s'); cte_wp_at (\<lambda>_. True) parent s'; cte_wp_at (\<lambda>_. True) slot s'\<rbrakk> \<Longrightarrow> (map_lift_over transform_cslot_ptr (cdt s'))(transform_cslot_ptr slot := map_option transform_cslot_ptr (Some parent)) = (map_lift_over transform_cslot_ptr (cdt s'))(transform_cslot_ptr slot \<mapsto> transform_cslot_ptr parent)
 2. dcorres (\<lambda>a b. True) ?R10 ?R'10 (KHeap_D.set_cap (transform_cslot_ptr slot) (Types_D.default_cap (translate_object_type type) (retype_transform_obj_ref type sz ptr) sz dev)) (CSpaceAcc_A.set_cap (Retype_A.default_cap type ptr sz dev) slot)
 3. \<lbrace>?Q14 cdl_cap.NullCap\<rbrace> set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent) \<lbrace>\<lambda>x. ?R10\<rbrace>
 4. \<lbrace>?Q'10\<rbrace> do y <- do dest_p <- gets (\<lambda>s. cdt s slot);
y <- do cdt <- gets cdt;
set_cdt (cdt(slot \<mapsto> parent))
od;
create_cap_ext parent slot dest_p
od;
set_original slot True
od \<lbrace>\<lambda>x. ?R'10\<rbrace>
 5. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. (the \<circ> opt_cap (transform_cslot_ptr slot)) s = cdl_cap.NullCap \<and> ((\<lambda>a. True) and ?Q14 ((the \<circ> opt_cap (transform_cslot_ptr slot)) s)) s) and (\<lambda>s. opt_cap (transform_cslot_ptr slot) s \<noteq> None)) s
 6. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdt s slot = None \<and> cte_wp_at (\<lambda>_. True) slot s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> cte_wp_at (\<lambda>_. True) slot s) and ?Q'10) s' proof (prove)
goal (5 subgoals):
 1. dcorres (\<lambda>a b. True) ?R10 ?R'10 (KHeap_D.set_cap (transform_cslot_ptr slot) (Types_D.default_cap (translate_object_type type) (retype_transform_obj_ref type sz ptr) sz dev)) (CSpaceAcc_A.set_cap (Retype_A.default_cap type ptr sz dev) slot)
 2. \<lbrace>?Q14 cdl_cap.NullCap\<rbrace> set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent) \<lbrace>\<lambda>x. ?R10\<rbrace>
 3. \<lbrace>?Q'10\<rbrace> do y <- do dest_p <- gets (\<lambda>s. cdt s slot);
y <- do cdt <- gets cdt;
set_cdt (cdt(slot \<mapsto> parent))
od;
create_cap_ext parent slot dest_p
od;
set_original slot True
od \<lbrace>\<lambda>x. ?R'10\<rbrace>
 4. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. (the \<circ> opt_cap (transform_cslot_ptr slot)) s = cdl_cap.NullCap \<and> ((\<lambda>a. True) and ?Q14 ((the \<circ> opt_cap (transform_cslot_ptr slot)) s)) s) and (\<lambda>s. opt_cap (transform_cslot_ptr slot) s \<noteq> None)) s
 5. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdt s slot = None \<and> cte_wp_at (\<lambda>_. True) slot s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> cte_wp_at (\<lambda>_. True) slot s) and ?Q'10) s' proof (prove)
goal (5 subgoals):
 1. dcorres dc ?R10 ?R'10 (KHeap_D.set_cap (transform_cslot_ptr slot) (Types_D.default_cap (translate_object_type type) (retype_transform_obj_ref type sz ptr) sz dev)) (CSpaceAcc_A.set_cap (Retype_A.default_cap type ptr sz dev) slot)
 2. \<lbrace>?Q14 cdl_cap.NullCap\<rbrace> set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent) \<lbrace>\<lambda>x. ?R10\<rbrace>
 3. \<lbrace>?Q'10\<rbrace> do y <- do dest_p <- gets (\<lambda>s. cdt s slot);
y <- do cdt <- gets cdt;
set_cdt (cdt(slot \<mapsto> parent))
od;
create_cap_ext parent slot dest_p
od;
set_original slot True
od \<lbrace>\<lambda>x. ?R'10\<rbrace>
 4. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. (the \<circ> opt_cap (transform_cslot_ptr slot)) s = cdl_cap.NullCap \<and> ((\<lambda>a. True) and ?Q14 ((the \<circ> opt_cap (transform_cslot_ptr slot)) s)) s) and (\<lambda>s. opt_cap (transform_cslot_ptr slot) s \<noteq> None)) s
 5. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdt s slot = None \<and> cte_wp_at (\<lambda>_. True) slot s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> cte_wp_at (\<lambda>_. True) slot s) and ?Q'10) s' proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q14 cdl_cap.NullCap\<rbrace> set_parent (transform_cslot_ptr slot) (transform_cslot_ptr parent) \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<lbrace>?Q'10\<rbrace> do y <- do dest_p <- gets (\<lambda>s. cdt s slot);
y <- do cdt <- gets cdt;
set_cdt (cdt(slot \<mapsto> parent))
od;
create_cap_ext parent slot dest_p
od;
set_original slot True
od \<lbrace>\<lambda>x s. valid_idle s \<and> fst slot \<noteq> idle_thread s \<and> valid_etcbs s\<rbrace>
 3. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. (the \<circ> opt_cap (transform_cslot_ptr slot)) s = cdl_cap.NullCap \<and> ((\<lambda>a. True) and ?Q14 ((the \<circ> opt_cap (transform_cslot_ptr slot)) s)) s) and (\<lambda>s. opt_cap (transform_cslot_ptr slot) s \<noteq> None)) s
 4. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdt s slot = None \<and> cte_wp_at (\<lambda>_. True) slot s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> cte_wp_at (\<lambda>_. True) slot s) and ?Q'10) s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>cte_wp_at (\<lambda>_. True) parent s' \<and> cte_wp_at ((=) cap.NullCap) slot s' \<and> not_idle_thread (fst slot) s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); transform s' = s\<rbrakk> \<Longrightarrow> the (opt_cap (transform_cslot_ptr slot) s) = cdl_cap.NullCap \<and> (\<exists>y. opt_cap (transform_cslot_ptr slot) s = Some y)
 2. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdt s slot = None \<and> cte_wp_at (\<lambda>_. True) slot s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> cte_wp_at (\<lambda>_. True) slot s) and (\<lambda>s. valid_idle s \<and> fst slot \<noteq> idle_thread s \<and> valid_etcbs s)) s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>True; (cte_wp_at (\<lambda>_. True) parent and cte_wp_at ((=) cap.NullCap) slot and not_idle_thread (fst slot) and valid_idle and valid_etcbs and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. cdt s slot = None \<and> cte_wp_at (\<lambda>_. True) slot s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> mdb_cte_at (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) \<and> cte_wp_at (\<lambda>_. True) parent s \<and> cte_wp_at (\<lambda>_. True) slot s) and (\<lambda>s. valid_idle s \<and> fst slot \<noteq> idle_thread s \<and> valid_etcbs s)) s' proof (prove)
goal (1 subgoal):
 1. \<And>s' cap. \<lbrakk>caps_of_state s' parent = Some cap; caps_of_state s' slot = Some cap.NullCap; fst slot \<noteq> idle_thread s'; valid_idle s'; valid_etcbs s'; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s' y = Some cap \<and> cap.NullCap \<noteq> cap) (cdt s')\<rbrakk> \<Longrightarrow> cdt s' slot = None \<and> mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s' y = Some cap) (cdt s') proof (prove)
goal (2 subgoals):
 1. \<And>s' cap. \<lbrakk>caps_of_state s' parent = Some cap; fst slot \<noteq> idle_thread s'; valid_idle s'; valid_etcbs s'; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s' y = Some cap \<and> cap.NullCap \<noteq> cap) (cdt s')\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s')
 2. \<And>s' cap. \<lbrakk>caps_of_state s' parent = Some cap; fst slot \<noteq> idle_thread s'; valid_idle s'; valid_etcbs s'; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s' y = Some cap \<and> cap.NullCap \<noteq> cap) (cdt s'); cdt s' slot = None\<rbrakk> \<Longrightarrow> cdt s' slot = None \<and> mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s' y = Some cap) (cdt s') proof (prove)
goal (1 subgoal):
 1. \<And>s' cap. \<lbrakk>caps_of_state s' parent = Some cap; fst slot \<noteq> idle_thread s'; valid_idle s'; valid_etcbs s'; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s' y = Some cap \<and> cap.NullCap \<noteq> cap) (cdt s'); cdt s' slot = None\<rbrakk> \<Longrightarrow> cdt s' slot = None \<and> mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s' y = Some cap) (cdt s') proof (prove)
goal:
No subgoals!