theory KHeap_DR

lemma always_empty_slot_NullCap_corres:
  "dcorres dc \<top>
           (weak_valid_mdb and not_idle_thread (fst slot) and
            cte_wp_at ((=) cap.NullCap) slot and valid_etcbs)
           (do y \<leftarrow> remove_parent (transform_cslot_ptr slot);
               KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
            od)
           (return ())" supply if_cong[cong] apply (simp add: remove_parent_def) apply (clarsimp simp: corres_underlying_def in_monad simpler_modify_def bind_def) apply (subst set_cap_is_noop_opt_cap) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (drule caps_of_state_transform_opt_cap) apply clarsimp apply (clarsimp simp: not_idle_thread_def) apply (clarsimp cong: opt_cap_objects_cong) apply (clarsimp simp: return_def transform_def) apply (rule ext) apply clarsimp apply (subgoal_tac "transform_cdt b (transform_cslot_ptr slot) = None") prefer 2 apply (rule transform_cdt_none) apply (erule cte_wp_at_weakenE, rule TrueI) apply (simp add: weak_valid_mdb_def) apply (clarsimp simp: weak_valid_mdb_def mdb_cte_at_def) apply (rule classical) apply (cases slot) apply clarsimp apply (erule allE)+ apply (erule (1) impE) apply (clarsimp simp: cte_wp_at_def) apply (cases slot) apply clarsimp apply (subgoal_tac "\<exists>p. (a,ba) = transform_cslot_ptr p") apply clarsimp apply (drule transform_cdt_some_rev) apply (erule cte_wp_at_weakenE, rule TrueI) apply (simp add: weak_valid_mdb_def) apply (clarsimp simp: weak_valid_mdb_def mdb_cte_at_def) apply (erule allE)+ apply (erule (1) impE) apply (clarsimp simp: cte_wp_at_def) apply (clarsimp simp: transform_cslot_ptr_def) apply (rule nat_bl_to_bin_surj) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (weak_valid_mdb and not_idle_thread (fst slot) and cte_wp_at ((=) cap.NullCap) slot and valid_etcbs) (do y <- remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (return ()) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (weak_valid_mdb and not_idle_thread (fst slot) and cte_wp_at ((=) cap.NullCap) slot and valid_etcbs) (do y <- remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (return ()) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (weak_valid_mdb and not_idle_thread (fst slot) and cte_wp_at ((=) cap.NullCap) slot and valid_etcbs) (do y <- modify (\<lambda>s. s\<lparr>cdl_cdt := \<lambda>x. if x = transform_cslot_ptr slot then None else if cdl_cdt s x = Some (transform_cslot_ptr slot) then cdl_cdt s (transform_cslot_ptr slot) else cdl_cdt s x\<rparr>);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (return ()) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap (transform b\<lparr>cdl_cdt := \<lambda>x. if x = transform_cslot_ptr slot then None else if cdl_cdt (transform b) x = Some (transform_cslot_ptr slot) then cdl_cdt (transform b) (transform_cslot_ptr slot) else cdl_cdt (transform b) x\<rparr>)). case x of (r, x) \<Rightarrow> transform b = x proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr slot) (transform b\<lparr>cdl_cdt := \<lambda>x. if x = transform_cslot_ptr slot then None else if cdl_cdt (transform b) x = Some (transform_cslot_ptr slot) then cdl_cdt (transform b) (transform_cslot_ptr slot) else cdl_cdt (transform b) x\<rparr>) = Some cdl_cap.NullCap
 2. \<And>b. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> \<exists>(r, y)\<in>fst (return () (transform b\<lparr>cdl_cdt := \<lambda>x. if x = transform_cslot_ptr slot then None else if cdl_cdt (transform b) x = Some (transform_cslot_ptr slot) then cdl_cdt (transform b) (transform_cslot_ptr slot) else cdl_cdt (transform b) x\<rparr>)). transform b = y proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; caps_of_state b slot = Some cap.NullCap; valid_etcbs b\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr slot) (transform b\<lparr>cdl_cdt := \<lambda>x. if x = transform_cslot_ptr slot then None else if cdl_cdt (transform b) x = Some (transform_cslot_ptr slot) then cdl_cdt (transform b) (transform_cslot_ptr slot) else cdl_cdt (transform b) x\<rparr>) = Some cdl_cap.NullCap
 2. \<And>b. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> \<exists>(r, y)\<in>fst (return () (transform b\<lparr>cdl_cdt := \<lambda>x. if x = transform_cslot_ptr slot then None else if cdl_cdt (transform b) x = Some (transform_cslot_ptr slot) then cdl_cdt (transform b) (transform_cslot_ptr slot) else cdl_cdt (transform b) x\<rparr>)). transform b = y proof (prove)
goal (4 subgoals):
 1. \<And>b. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; valid_etcbs b\<rbrakk> \<Longrightarrow> valid_etcbs b
 2. \<And>b. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; valid_etcbs b\<rbrakk> \<Longrightarrow> fst slot \<noteq> idle_thread b
 3. \<And>b. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; valid_etcbs b; opt_cap (transform_cslot_ptr slot) (transform b) = Some (transform_cap cap.NullCap)\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr slot) (transform b\<lparr>cdl_cdt := \<lambda>x. if x = transform_cslot_ptr slot then None else if cdl_cdt (transform b) x = Some (transform_cslot_ptr slot) then cdl_cdt (transform b) (transform_cslot_ptr slot) else cdl_cdt (transform b) x\<rparr>) = Some cdl_cap.NullCap
 4. \<And>b. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> \<exists>(r, y)\<in>fst (return () (transform b\<lparr>cdl_cdt := \<lambda>x. if x = transform_cslot_ptr slot then None else if cdl_cdt (transform b) x = Some (transform_cslot_ptr slot) then cdl_cdt (transform b) (transform_cslot_ptr slot) else cdl_cdt (transform b) x\<rparr>)). transform b = y proof (prove)
goal (3 subgoals):
 1. \<And>b. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; valid_etcbs b\<rbrakk> \<Longrightarrow> fst slot \<noteq> idle_thread b
 2. \<And>b. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; valid_etcbs b; opt_cap (transform_cslot_ptr slot) (transform b) = Some (transform_cap cap.NullCap)\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr slot) (transform b\<lparr>cdl_cdt := \<lambda>x. if x = transform_cslot_ptr slot then None else if cdl_cdt (transform b) x = Some (transform_cslot_ptr slot) then cdl_cdt (transform b) (transform_cslot_ptr slot) else cdl_cdt (transform b) x\<rparr>) = Some cdl_cap.NullCap
 3. \<And>b. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> \<exists>(r, y)\<in>fst (return () (transform b\<lparr>cdl_cdt := \<lambda>x. if x = transform_cslot_ptr slot then None else if cdl_cdt (transform b) x = Some (transform_cslot_ptr slot) then cdl_cdt (transform b) (transform_cslot_ptr slot) else cdl_cdt (transform b) x\<rparr>)). transform b = y proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; valid_etcbs b; opt_cap (transform_cslot_ptr slot) (transform b) = Some (transform_cap cap.NullCap)\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr slot) (transform b\<lparr>cdl_cdt := \<lambda>x. if x = transform_cslot_ptr slot then None else if cdl_cdt (transform b) x = Some (transform_cslot_ptr slot) then cdl_cdt (transform b) (transform_cslot_ptr slot) else cdl_cdt (transform b) x\<rparr>) = Some cdl_cap.NullCap
 2. \<And>b. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> \<exists>(r, y)\<in>fst (return () (transform b\<lparr>cdl_cdt := \<lambda>x. if x = transform_cslot_ptr slot then None else if cdl_cdt (transform b) x = Some (transform_cslot_ptr slot) then cdl_cdt (transform b) (transform_cslot_ptr slot) else cdl_cdt (transform b) x\<rparr>)). transform b = y proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> \<exists>(r, y)\<in>fst (return () (transform b\<lparr>cdl_cdt := \<lambda>x. if x = transform_cslot_ptr slot then None else if cdl_cdt (transform b) x = Some (transform_cslot_ptr slot) then cdl_cdt (transform b) (transform_cslot_ptr slot) else cdl_cdt (transform b) x\<rparr>)). transform b = y proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> transform_cdt b = (\<lambda>x. if x = transform_cslot_ptr slot then None else if transform_cdt b x = Some (transform_cslot_ptr slot) then transform_cdt b (transform_cslot_ptr slot) else transform_cdt b x) proof (prove)
goal (1 subgoal):
 1. \<And>b x. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> transform_cdt b x = (if x = transform_cslot_ptr slot then None else if transform_cdt b x = Some (transform_cslot_ptr slot) then transform_cdt b (transform_cslot_ptr slot) else transform_cdt b x) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> (transform_cdt b (a, ba) = Some (transform_cslot_ptr slot) \<longrightarrow> ((a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) \<and> ((a, ba) \<noteq> transform_cslot_ptr slot \<longrightarrow> Some (transform_cslot_ptr slot) = transform_cdt b (transform_cslot_ptr slot))) \<and> (transform_cdt b (a, ba) \<noteq> Some (transform_cslot_ptr slot) \<longrightarrow> (a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b; transform_cdt b (transform_cslot_ptr slot) = None\<rbrakk> \<Longrightarrow> (transform_cdt b (a, ba) = Some (transform_cslot_ptr slot) \<longrightarrow> ((a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) \<and> ((a, ba) \<noteq> transform_cslot_ptr slot \<longrightarrow> Some (transform_cslot_ptr slot) = transform_cdt b (transform_cslot_ptr slot))) \<and> (transform_cdt b (a, ba) \<noteq> Some (transform_cslot_ptr slot) \<longrightarrow> (a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None)
 2. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None proof (prove)
goal (2 subgoals):
 1. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None
 2. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b; transform_cdt b (transform_cslot_ptr slot) = None\<rbrakk> \<Longrightarrow> (transform_cdt b (a, ba) = Some (transform_cslot_ptr slot) \<longrightarrow> ((a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) \<and> ((a, ba) \<noteq> transform_cslot_ptr slot \<longrightarrow> Some (transform_cslot_ptr slot) = transform_cdt b (transform_cslot_ptr slot))) \<and> (transform_cdt b (a, ba) \<noteq> Some (transform_cslot_ptr slot) \<longrightarrow> (a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) proof (prove)
goal (4 subgoals):
 1. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot b
 2. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)
 3. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> cdt b slot = None
 4. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b; transform_cdt b (transform_cslot_ptr slot) = None\<rbrakk> \<Longrightarrow> (transform_cdt b (a, ba) = Some (transform_cslot_ptr slot) \<longrightarrow> ((a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) \<and> ((a, ba) \<noteq> transform_cslot_ptr slot \<longrightarrow> Some (transform_cslot_ptr slot) = transform_cdt b (transform_cslot_ptr slot))) \<and> (transform_cdt b (a, ba) \<noteq> Some (transform_cslot_ptr slot) \<longrightarrow> (a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) proof (prove)
goal (3 subgoals):
 1. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)
 2. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> cdt b slot = None
 3. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b; transform_cdt b (transform_cslot_ptr slot) = None\<rbrakk> \<Longrightarrow> (transform_cdt b (a, ba) = Some (transform_cslot_ptr slot) \<longrightarrow> ((a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) \<and> ((a, ba) \<noteq> transform_cslot_ptr slot \<longrightarrow> Some (transform_cslot_ptr slot) = transform_cdt b (transform_cslot_ptr slot))) \<and> (transform_cdt b (a, ba) \<noteq> Some (transform_cslot_ptr slot) \<longrightarrow> (a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b\<rbrakk> \<Longrightarrow> cdt b slot = None
 2. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b; transform_cdt b (transform_cslot_ptr slot) = None\<rbrakk> \<Longrightarrow> (transform_cdt b (a, ba) = Some (transform_cslot_ptr slot) \<longrightarrow> ((a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) \<and> ((a, ba) \<noteq> transform_cslot_ptr slot \<longrightarrow> Some (transform_cslot_ptr slot) = transform_cdt b (transform_cslot_ptr slot))) \<and> (transform_cdt b (a, ba) \<noteq> Some (transform_cslot_ptr slot) \<longrightarrow> (a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b; \<forall>a ba aa bb. cdt b (aa, bb) = Some (a, ba) \<longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (a, ba) b \<and> cte_wp_at ((\<noteq>) cap.NullCap) (aa, bb) b; no_mloop (cdt b)\<rbrakk> \<Longrightarrow> cdt b slot = None
 2. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b; transform_cdt b (transform_cslot_ptr slot) = None\<rbrakk> \<Longrightarrow> (transform_cdt b (a, ba) = Some (transform_cslot_ptr slot) \<longrightarrow> ((a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) \<and> ((a, ba) \<noteq> transform_cslot_ptr slot \<longrightarrow> Some (transform_cslot_ptr slot) = transform_cdt b (transform_cslot_ptr slot))) \<and> (transform_cdt b (a, ba) \<noteq> Some (transform_cslot_ptr slot) \<longrightarrow> (a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b; \<forall>a ba aa bb. cdt b (aa, bb) = Some (a, ba) \<longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (a, ba) b \<and> cte_wp_at ((\<noteq>) cap.NullCap) (aa, bb) b; no_mloop (cdt b); cdt b slot \<noteq> None\<rbrakk> \<Longrightarrow> cdt b slot = None
 2. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b; transform_cdt b (transform_cslot_ptr slot) = None\<rbrakk> \<Longrightarrow> (transform_cdt b (a, ba) = Some (transform_cslot_ptr slot) \<longrightarrow> ((a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) \<and> ((a, ba) \<noteq> transform_cslot_ptr slot \<longrightarrow> Some (transform_cslot_ptr slot) = transform_cdt b (transform_cslot_ptr slot))) \<and> (transform_cdt b (a, ba) \<noteq> Some (transform_cslot_ptr slot) \<longrightarrow> (a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba. \<lbrakk>not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b; \<forall>a ba aa bb. cdt b (aa, bb) = Some (a, ba) \<longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (a, ba) b \<and> cte_wp_at ((\<noteq>) cap.NullCap) (aa, bb) b; no_mloop (cdt b); cdt b slot \<noteq> None; slot = (a, ba)\<rbrakk> \<Longrightarrow> cdt b slot = None
 2. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b; transform_cdt b (transform_cslot_ptr slot) = None\<rbrakk> \<Longrightarrow> (transform_cdt b (a, ba) = Some (transform_cslot_ptr slot) \<longrightarrow> ((a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) \<and> ((a, ba) \<noteq> transform_cslot_ptr slot \<longrightarrow> Some (transform_cslot_ptr slot) = transform_cdt b (transform_cslot_ptr slot))) \<and> (transform_cdt b (a, ba) \<noteq> Some (transform_cslot_ptr slot) \<longrightarrow> (a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba aa bb. \<lbrakk>not_idle_thread a b; cte_wp_at ((=) cap.NullCap) (a, ba) b; valid_etcbs b; \<forall>a ba aa bb. cdt b (aa, bb) = Some (a, ba) \<longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (a, ba) b \<and> cte_wp_at ((\<noteq>) cap.NullCap) (aa, bb) b; no_mloop (cdt b); slot = (a, ba); cdt b (a, ba) = Some (aa, bb)\<rbrakk> \<Longrightarrow> False
 2. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b; transform_cdt b (transform_cslot_ptr slot) = None\<rbrakk> \<Longrightarrow> (transform_cdt b (a, ba) = Some (transform_cslot_ptr slot) \<longrightarrow> ((a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) \<and> ((a, ba) \<noteq> transform_cslot_ptr slot \<longrightarrow> Some (transform_cslot_ptr slot) = transform_cdt b (transform_cslot_ptr slot))) \<and> (transform_cdt b (a, ba) \<noteq> Some (transform_cslot_ptr slot) \<longrightarrow> (a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba aa bb. \<lbrakk>not_idle_thread a b; cte_wp_at ((=) cap.NullCap) (a, ba) b; valid_etcbs b; no_mloop (cdt b); slot = (a, ba); cdt b (a, ba) = Some (aa, bb); cdt b (?a76 b a ba aa bb, ?b78 b a ba aa bb) = Some (?a72 b a ba aa bb, ?b74 b a ba aa bb) \<longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (?a72 b a ba aa bb, ?b74 b a ba aa bb) b \<and> cte_wp_at ((\<noteq>) cap.NullCap) (?a76 b a ba aa bb, ?b78 b a ba aa bb) b\<rbrakk> \<Longrightarrow> False
 2. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b; transform_cdt b (transform_cslot_ptr slot) = None\<rbrakk> \<Longrightarrow> (transform_cdt b (a, ba) = Some (transform_cslot_ptr slot) \<longrightarrow> ((a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) \<and> ((a, ba) \<noteq> transform_cslot_ptr slot \<longrightarrow> Some (transform_cslot_ptr slot) = transform_cdt b (transform_cslot_ptr slot))) \<and> (transform_cdt b (a, ba) \<noteq> Some (transform_cslot_ptr slot) \<longrightarrow> (a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba aa bb. \<lbrakk>not_idle_thread a b; cte_wp_at ((=) cap.NullCap) (a, ba) b; valid_etcbs b; no_mloop (cdt b); slot = (a, ba); cdt b (a, ba) = Some (aa, bb); cte_wp_at ((\<noteq>) cap.NullCap) (aa, bb) b \<and> cte_wp_at ((\<noteq>) cap.NullCap) (a, ba) b\<rbrakk> \<Longrightarrow> False
 2. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b; transform_cdt b (transform_cslot_ptr slot) = None\<rbrakk> \<Longrightarrow> (transform_cdt b (a, ba) = Some (transform_cslot_ptr slot) \<longrightarrow> ((a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) \<and> ((a, ba) \<noteq> transform_cslot_ptr slot \<longrightarrow> Some (transform_cslot_ptr slot) = transform_cdt b (transform_cslot_ptr slot))) \<and> (transform_cdt b (a, ba) \<noteq> Some (transform_cslot_ptr slot) \<longrightarrow> (a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b; transform_cdt b (transform_cslot_ptr slot) = None\<rbrakk> \<Longrightarrow> (transform_cdt b (a, ba) = Some (transform_cslot_ptr slot) \<longrightarrow> ((a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) \<and> ((a, ba) \<noteq> transform_cslot_ptr slot \<longrightarrow> Some (transform_cslot_ptr slot) = transform_cdt b (transform_cslot_ptr slot))) \<and> (transform_cdt b (a, ba) \<noteq> Some (transform_cslot_ptr slot) \<longrightarrow> (a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba aa bb. \<lbrakk>weak_valid_mdb b; not_idle_thread (fst slot) b; cte_wp_at ((=) cap.NullCap) slot b; valid_etcbs b; transform_cdt b (transform_cslot_ptr slot) = None; slot = (aa, bb)\<rbrakk> \<Longrightarrow> (transform_cdt b (a, ba) = Some (transform_cslot_ptr slot) \<longrightarrow> ((a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) \<and> ((a, ba) \<noteq> transform_cslot_ptr slot \<longrightarrow> Some (transform_cslot_ptr slot) = transform_cdt b (transform_cslot_ptr slot))) \<and> (transform_cdt b (a, ba) \<noteq> Some (transform_cslot_ptr slot) \<longrightarrow> (a, ba) = transform_cslot_ptr slot \<longrightarrow> transform_cdt b (transform_cslot_ptr slot) = None) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba aa bb. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); transform_cdt b (a, ba) = Some (transform_cslot_ptr (aa, bb))\<rbrakk> \<Longrightarrow> (a, ba) = transform_cslot_ptr (aa, bb) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba aa bb. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); transform_cdt b (a, ba) = Some (transform_cslot_ptr (aa, bb)); \<exists>p. (a, ba) = transform_cslot_ptr p\<rbrakk> \<Longrightarrow> (a, ba) = transform_cslot_ptr (aa, bb)
 2. \<And>b a ba aa bb. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); transform_cdt b (a, ba) = Some (transform_cslot_ptr (aa, bb))\<rbrakk> \<Longrightarrow> \<exists>p. (a, ba) = transform_cslot_ptr p proof (prove)
goal (2 subgoals):
 1. \<And>b a ba aa bb ab bc. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); transform_cdt b (transform_cslot_ptr (ab, bc)) = Some (transform_cslot_ptr (aa, bb)); (a, ba) = transform_cslot_ptr (ab, bc)\<rbrakk> \<Longrightarrow> transform_cslot_ptr (ab, bc) = transform_cslot_ptr (aa, bb)
 2. \<And>b a ba aa bb. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); transform_cdt b (a, ba) = Some (transform_cslot_ptr (aa, bb))\<rbrakk> \<Longrightarrow> \<exists>p. (a, ba) = transform_cslot_ptr p proof (prove)
goal (4 subgoals):
 1. \<And>b a ba aa bb ab bc. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); (a, ba) = transform_cslot_ptr (ab, bc)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (aa, bb) b
 2. \<And>b a ba aa bb ab bc. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); (a, ba) = transform_cslot_ptr (ab, bc)\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)
 3. \<And>b a ba aa bb ab bc. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); (a, ba) = transform_cslot_ptr (ab, bc); \<exists>slot_b. transform_cslot_ptr slot_b = transform_cslot_ptr (ab, bc) \<and> cdt b slot_b = Some (aa, bb)\<rbrakk> \<Longrightarrow> transform_cslot_ptr (ab, bc) = transform_cslot_ptr (aa, bb)
 4. \<And>b a ba aa bb. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); transform_cdt b (a, ba) = Some (transform_cslot_ptr (aa, bb))\<rbrakk> \<Longrightarrow> \<exists>p. (a, ba) = transform_cslot_ptr p proof (prove)
goal (3 subgoals):
 1. \<And>b a ba aa bb ab bc. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); (a, ba) = transform_cslot_ptr (ab, bc)\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) b) (cdt b)
 2. \<And>b a ba aa bb ab bc. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); (a, ba) = transform_cslot_ptr (ab, bc); \<exists>slot_b. transform_cslot_ptr slot_b = transform_cslot_ptr (ab, bc) \<and> cdt b slot_b = Some (aa, bb)\<rbrakk> \<Longrightarrow> transform_cslot_ptr (ab, bc) = transform_cslot_ptr (aa, bb)
 3. \<And>b a ba aa bb. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); transform_cdt b (a, ba) = Some (transform_cslot_ptr (aa, bb))\<rbrakk> \<Longrightarrow> \<exists>p. (a, ba) = transform_cslot_ptr p proof (prove)
goal (2 subgoals):
 1. \<And>b a ba aa bb ab bc. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); (a, ba) = transform_cslot_ptr (ab, bc); \<exists>slot_b. transform_cslot_ptr slot_b = transform_cslot_ptr (ab, bc) \<and> cdt b slot_b = Some (aa, bb)\<rbrakk> \<Longrightarrow> transform_cslot_ptr (ab, bc) = transform_cslot_ptr (aa, bb)
 2. \<And>b a ba aa bb. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); transform_cdt b (a, ba) = Some (transform_cslot_ptr (aa, bb))\<rbrakk> \<Longrightarrow> \<exists>p. (a, ba) = transform_cslot_ptr p proof (prove)
goal (2 subgoals):
 1. \<And>b a ba aa bb ab bc ac bd. \<lbrakk>not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); (a, ba) = transform_cslot_ptr (ab, bc); \<forall>a ba aa bb. cdt b (aa, bb) = Some (a, ba) \<longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (a, ba) b \<and> cte_wp_at ((\<noteq>) cap.NullCap) (aa, bb) b; no_mloop (cdt b); transform_cslot_ptr (ac, bd) = transform_cslot_ptr (ab, bc); cdt b (ac, bd) = Some (aa, bb)\<rbrakk> \<Longrightarrow> transform_cslot_ptr (ab, bc) = transform_cslot_ptr (aa, bb)
 2. \<And>b a ba aa bb. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); transform_cdt b (a, ba) = Some (transform_cslot_ptr (aa, bb))\<rbrakk> \<Longrightarrow> \<exists>p. (a, ba) = transform_cslot_ptr p proof (prove)
goal (2 subgoals):
 1. \<And>b a ba aa bb ab bc ac bd. \<lbrakk>not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); (a, ba) = transform_cslot_ptr (ab, bc); no_mloop (cdt b); transform_cslot_ptr (ac, bd) = transform_cslot_ptr (ab, bc); cdt b (ac, bd) = Some (aa, bb); cdt b (?a106 b a ba aa bb ab bc ac bd, ?b108 b a ba aa bb ab bc ac bd) = Some (?a102 b a ba aa bb ab bc ac bd, ?b104 b a ba aa bb ab bc ac bd) \<longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) (?a102 b a ba aa bb ab bc ac bd, ?b104 b a ba aa bb ab bc ac bd) b \<and> cte_wp_at ((\<noteq>) cap.NullCap) (?a106 b a ba aa bb ab bc ac bd, ?b108 b a ba aa bb ab bc ac bd) b\<rbrakk> \<Longrightarrow> transform_cslot_ptr (ab, bc) = transform_cslot_ptr (aa, bb)
 2. \<And>b a ba aa bb. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); transform_cdt b (a, ba) = Some (transform_cslot_ptr (aa, bb))\<rbrakk> \<Longrightarrow> \<exists>p. (a, ba) = transform_cslot_ptr p proof (prove)
goal (2 subgoals):
 1. \<And>b a ba aa bb ab bc ac bd. \<lbrakk>not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); (a, ba) = transform_cslot_ptr (ab, bc); no_mloop (cdt b); transform_cslot_ptr (ac, bd) = transform_cslot_ptr (ab, bc); cdt b (ac, bd) = Some (aa, bb); cte_wp_at ((\<noteq>) cap.NullCap) (aa, bb) b \<and> cte_wp_at ((\<noteq>) cap.NullCap) (ac, bd) b\<rbrakk> \<Longrightarrow> transform_cslot_ptr (ab, bc) = transform_cslot_ptr (aa, bb)
 2. \<And>b a ba aa bb. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); transform_cdt b (a, ba) = Some (transform_cslot_ptr (aa, bb))\<rbrakk> \<Longrightarrow> \<exists>p. (a, ba) = transform_cslot_ptr p proof (prove)
goal (1 subgoal):
 1. \<And>b a ba aa bb. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (transform_cslot_ptr (aa, bb)) = None; slot = (aa, bb); transform_cdt b (a, ba) = Some (transform_cslot_ptr (aa, bb))\<rbrakk> \<Longrightarrow> \<exists>p. (a, ba) = transform_cslot_ptr p proof (prove)
goal (1 subgoal):
 1. \<And>b a ba aa bb. \<lbrakk>weak_valid_mdb b; not_idle_thread aa b; cte_wp_at ((=) cap.NullCap) (aa, bb) b; valid_etcbs b; transform_cdt b (aa, nat (bl_to_bin bb)) = None; slot = (aa, bb); transform_cdt b (a, ba) = Some (aa, nat (bl_to_bin bb))\<rbrakk> \<Longrightarrow> \<exists>b. ba = nat (bl_to_bin b) proof (prove)
goal:
No subgoals!