theory KHeap_DR

lemma dummy_remove_cdt_pd_slot:
  "dcorres dc \<top> ( (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and page_directory_at a)
    (remove_parent (a,y)) (return x)" supply if_cong[cong] apply (rule dcorres_expand_pfx) apply (clarsimp simp:remove_parent_def corres_underlying_def return_def simpler_modify_def) apply (clarsimp simp:remove_parent_def exs_valid_def simpler_modify_def transform_def) apply (rule ext) apply (clarsimp simp:transform_cdt_def| rule conjI)+ apply (clarsimp simp: map_lift_over_def transform_cdt_slot_inj_on_mdb_cte_at split:if_splits) apply (frule_tac slot="(aa,b)" in mdb_cte_at_cte_wp_at) apply simp apply (drule page_directory_not_in_cdt) apply (simp add:transform_cslot_ptr_def)+ apply (clarsimp simp:map_lift_over_def transform_cdt_slot_inj_on_mdb_cte_at split:if_splits) apply (frule_tac slot'="(a,bb)" in mdb_cte_at_cte_wp_at') apply simp apply (drule page_directory_not_in_cdt) apply simp+ apply (clarsimp simp: option_map_def  map_lift_over_def transform_cdt_slot_inj_on_mdb_cte_at
      split:if_splits option.splits| rule conjI)+ apply (clarsimp simp:transform_cslot_ptr_def) apply (frule_tac slot="(a,bc)" in mdb_cte_at_cte_wp_at) apply simp apply (drule page_directory_not_in_cdt) apply simp+ apply (clarsimp simp: transform_cslot_ptr_def) apply (frule_tac slot="(a,bc)" in mdb_cte_at_cte_wp_at) apply simp apply (drule page_directory_not_in_cdt) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a) (remove_parent (a, y)) (return x) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a) (remove_parent (a, y)) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s = transform s'; True; ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) a) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (remove_parent (a, y)) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'\<rbrakk> \<Longrightarrow> transform s' = transform s'\<lparr>cdl_cdt := \<lambda>x. if x = (a, y) then None else if cdl_cdt (transform s') x = Some (a, y) then cdl_cdt (transform s') (a, y) else cdl_cdt (transform s') x\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'\<rbrakk> \<Longrightarrow> transform_cdt s' = (\<lambda>x. if x = (a, y) then None else if transform_cdt s' x = Some (a, y) then transform_cdt s' (a, y) else transform_cdt s' x) proof (prove)
goal (1 subgoal):
 1. \<And>s' x. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'\<rbrakk> \<Longrightarrow> transform_cdt s' x = (if x = (a, y) then None else if transform_cdt s' x = Some (a, y) then transform_cdt s' (a, y) else transform_cdt s' x) proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; map_lift_over transform_cslot_ptr (cdt s') (a, y) = Some (a, y)\<rbrakk> \<Longrightarrow> False
 2. \<And>s' aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; map_lift_over transform_cslot_ptr (cdt s') (aa, b) = Some (a, y)\<rbrakk> \<Longrightarrow> (aa = a \<longrightarrow> b \<noteq> y) \<longrightarrow> Some (a, y) = map_lift_over transform_cslot_ptr (cdt s') (a, y)
 3. \<And>s' aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (aa, b) \<noteq> Some (a, y) \<longrightarrow> aa = a \<and> b = y \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (a, y) = None proof (prove)
goal (3 subgoals):
 1. \<And>s' aa b aaa ab ba bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; transform_cslot_ptr (aa, b) = (a, y); cdt s' (aa, b) = Some (ab, ba); cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (a, y)) = Some (aaa, bb); transform_cslot_ptr (aaa, bb) = (a, y)\<rbrakk> \<Longrightarrow> False
 2. \<And>s' aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; map_lift_over transform_cslot_ptr (cdt s') (aa, b) = Some (a, y)\<rbrakk> \<Longrightarrow> (aa = a \<longrightarrow> b \<noteq> y) \<longrightarrow> Some (a, y) = map_lift_over transform_cslot_ptr (cdt s') (a, y)
 3. \<And>s' aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (aa, b) \<noteq> Some (a, y) \<longrightarrow> aa = a \<and> b = y \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (a, y) = None proof (prove)
goal (4 subgoals):
 1. \<And>s' aa b aaa ab ba bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; transform_cslot_ptr (aa, b) = (a, y); cdt s' (aa, b) = Some (ab, ba); cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (a, y)) = Some (aaa, bb); transform_cslot_ptr (aaa, bb) = (a, y)\<rbrakk> \<Longrightarrow> cdt s' (aa, b) = Some (?slot'89 s' aa b aaa ab ba bb)
 2. \<And>s' aa b aaa ab ba bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; transform_cslot_ptr (aa, b) = (a, y); cdt s' (aa, b) = Some (ab, ba); cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (a, y)) = Some (aaa, bb); transform_cslot_ptr (aaa, bb) = (a, y); cte_wp_at ((\<noteq>) cap.NullCap) (aa, b) s'\<rbrakk> \<Longrightarrow> False
 3. \<And>s' aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; map_lift_over transform_cslot_ptr (cdt s') (aa, b) = Some (a, y)\<rbrakk> \<Longrightarrow> (aa = a \<longrightarrow> b \<noteq> y) \<longrightarrow> Some (a, y) = map_lift_over transform_cslot_ptr (cdt s') (a, y)
 4. \<And>s' aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (aa, b) \<noteq> Some (a, y) \<longrightarrow> aa = a \<and> b = y \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (a, y) = None proof (prove)
goal (3 subgoals):
 1. \<And>s' aa b aaa ab ba bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; transform_cslot_ptr (aa, b) = (a, y); cdt s' (aa, b) = Some (ab, ba); cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (a, y)) = Some (aaa, bb); transform_cslot_ptr (aaa, bb) = (a, y); cte_wp_at ((\<noteq>) cap.NullCap) (aa, b) s'\<rbrakk> \<Longrightarrow> False
 2. \<And>s' aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; map_lift_over transform_cslot_ptr (cdt s') (aa, b) = Some (a, y)\<rbrakk> \<Longrightarrow> (aa = a \<longrightarrow> b \<noteq> y) \<longrightarrow> Some (a, y) = map_lift_over transform_cslot_ptr (cdt s') (a, y)
 3. \<And>s' aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (aa, b) \<noteq> Some (a, y) \<longrightarrow> aa = a \<and> b = y \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (a, y) = None proof (prove)
goal (4 subgoals):
 1. \<And>s' aa b aaa ab ba bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; transform_cslot_ptr (aa, b) = (a, y); cdt s' (aa, b) = Some (ab, ba); cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (a, y)) = Some (aaa, bb); transform_cslot_ptr (aaa, bb) = (a, y); cte_wp_at ((\<noteq>) cap.NullCap) (aa, b) s'\<rbrakk> \<Longrightarrow> cte_wp_at (?P92 s' aa b aaa ab ba bb) (a, ?ba92 s' aa b aaa ab ba bb) s'
 2. \<And>s' aa b aaa ab ba bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; transform_cslot_ptr (aa, b) = (a, y); cdt s' (aa, b) = Some (ab, ba); cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (a, y)) = Some (aaa, bb); transform_cslot_ptr (aaa, bb) = (a, y); cte_wp_at ((\<noteq>) cap.NullCap) (aa, b) s'; False\<rbrakk> \<Longrightarrow> False
 3. \<And>s' aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; map_lift_over transform_cslot_ptr (cdt s') (aa, b) = Some (a, y)\<rbrakk> \<Longrightarrow> (aa = a \<longrightarrow> b \<noteq> y) \<longrightarrow> Some (a, y) = map_lift_over transform_cslot_ptr (cdt s') (a, y)
 4. \<And>s' aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (aa, b) \<noteq> Some (a, y) \<longrightarrow> aa = a \<and> b = y \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (a, y) = None proof (prove)
goal (2 subgoals):
 1. \<And>s' aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; map_lift_over (\<lambda>(a, b). (a, nat (bl_to_bin b))) (cdt s') (aa, b) = Some (a, y)\<rbrakk> \<Longrightarrow> (aa = a \<longrightarrow> b \<noteq> y) \<longrightarrow> Some (a, y) = map_lift_over (\<lambda>(a, b). (a, nat (bl_to_bin b))) (cdt s') (a, y)
 2. \<And>s' aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (aa, b) \<noteq> Some (a, y) \<longrightarrow> aa = a \<and> b = y \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (a, y) = None proof (prove)
goal (2 subgoals):
 1. \<And>s' aa ba bb aaa bc. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s') \<union> ran (cdt s')); cdt s' (aa, ba) = Some (aaa, bc); cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (aa, nat (bl_to_bin ba))) = Some (a, bb); y = nat (bl_to_bin bb)\<rbrakk> \<Longrightarrow> ((\<exists>b. nat (bl_to_bin b) = nat (bl_to_bin bb) \<and> (a, b) \<in> dom (cdt s')) \<longrightarrow> (aa = a \<longrightarrow> nat (bl_to_bin ba) \<noteq> nat (bl_to_bin bb)) \<longrightarrow> Some (a, nat (bl_to_bin bb)) = map_option (\<lambda>(a, b). (a, nat (bl_to_bin b))) (cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (a, nat (bl_to_bin bb))))) \<and> ((\<forall>b. nat (bl_to_bin b) = nat (bl_to_bin bb) \<longrightarrow> (a, b) \<notin> dom (cdt s')) \<longrightarrow> aa = a \<and> nat (bl_to_bin ba) = nat (bl_to_bin bb))
 2. \<And>s' aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (aa, b) \<noteq> Some (a, y) \<longrightarrow> aa = a \<and> b = y \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (a, y) = None proof (prove)
goal (3 subgoals):
 1. \<And>s' aa ba bb aaa bc. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s') \<union> ran (cdt s')); cdt s' (aa, ba) = Some (aaa, bc); cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (aa, nat (bl_to_bin ba))) = Some (a, bb); y = nat (bl_to_bin bb)\<rbrakk> \<Longrightarrow> cdt s' (?slot138 s' aa ba bb aaa bc) = Some (a, bb)
 2. \<And>s' aa ba bb aaa bc. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s') \<union> ran (cdt s')); cdt s' (aa, ba) = Some (aaa, bc); cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (aa, nat (bl_to_bin ba))) = Some (a, bb); y = nat (bl_to_bin bb); cte_wp_at ((\<noteq>) cap.NullCap) (a, bb) s'\<rbrakk> \<Longrightarrow> ((\<exists>b. nat (bl_to_bin b) = nat (bl_to_bin bb) \<and> (a, b) \<in> dom (cdt s')) \<longrightarrow> (aa = a \<longrightarrow> nat (bl_to_bin ba) \<noteq> nat (bl_to_bin bb)) \<longrightarrow> Some (a, nat (bl_to_bin bb)) = map_option (\<lambda>(a, b). (a, nat (bl_to_bin b))) (cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (a, nat (bl_to_bin bb))))) \<and> ((\<forall>b. nat (bl_to_bin b) = nat (bl_to_bin bb) \<longrightarrow> (a, b) \<notin> dom (cdt s')) \<longrightarrow> aa = a \<and> nat (bl_to_bin ba) = nat (bl_to_bin bb))
 3. \<And>s' aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (aa, b) \<noteq> Some (a, y) \<longrightarrow> aa = a \<and> b = y \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (a, y) = None proof (prove)
goal (2 subgoals):
 1. \<And>s' aa ba bb aaa bc. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s') \<union> ran (cdt s')); cdt s' (aa, ba) = Some (aaa, bc); cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (aa, nat (bl_to_bin ba))) = Some (a, bb); y = nat (bl_to_bin bb); cte_wp_at ((\<noteq>) cap.NullCap) (a, bb) s'\<rbrakk> \<Longrightarrow> ((\<exists>b. nat (bl_to_bin b) = nat (bl_to_bin bb) \<and> (a, b) \<in> dom (cdt s')) \<longrightarrow> (aa = a \<longrightarrow> nat (bl_to_bin ba) \<noteq> nat (bl_to_bin bb)) \<longrightarrow> Some (a, nat (bl_to_bin bb)) = map_option (\<lambda>(a, b). (a, nat (bl_to_bin b))) (cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (a, nat (bl_to_bin bb))))) \<and> ((\<forall>b. nat (bl_to_bin b) = nat (bl_to_bin bb) \<longrightarrow> (a, b) \<notin> dom (cdt s')) \<longrightarrow> aa = a \<and> nat (bl_to_bin ba) = nat (bl_to_bin bb))
 2. \<And>s' aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (aa, b) \<noteq> Some (a, y) \<longrightarrow> aa = a \<and> b = y \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (a, y) = None proof (prove)
goal (3 subgoals):
 1. \<And>s' aa ba bb aaa bc. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s') \<union> ran (cdt s')); cdt s' (aa, ba) = Some (aaa, bc); cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (aa, nat (bl_to_bin ba))) = Some (a, bb); y = nat (bl_to_bin bb); cte_wp_at ((\<noteq>) cap.NullCap) (a, bb) s'\<rbrakk> \<Longrightarrow> cte_wp_at (?P140 s' aa ba bb aaa bc) (a, ?ba140 s' aa ba bb aaa bc) s'
 2. \<And>s' aa ba bb aaa bc. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; inj_on (\<lambda>(a, b). (a, nat (bl_to_bin b))) (dom (cdt s') \<union> ran (cdt s')); cdt s' (aa, ba) = Some (aaa, bc); cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (aa, nat (bl_to_bin ba))) = Some (a, bb); y = nat (bl_to_bin bb); cte_wp_at ((\<noteq>) cap.NullCap) (a, bb) s'; False\<rbrakk> \<Longrightarrow> ((\<exists>b. nat (bl_to_bin b) = nat (bl_to_bin bb) \<and> (a, b) \<in> dom (cdt s')) \<longrightarrow> (aa = a \<longrightarrow> nat (bl_to_bin ba) \<noteq> nat (bl_to_bin bb)) \<longrightarrow> Some (a, nat (bl_to_bin bb)) = map_option (\<lambda>(a, b). (a, nat (bl_to_bin b))) (cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (a, nat (bl_to_bin bb))))) \<and> ((\<forall>b. nat (bl_to_bin b) = nat (bl_to_bin bb) \<longrightarrow> (a, b) \<notin> dom (cdt s')) \<longrightarrow> aa = a \<and> nat (bl_to_bin ba) = nat (bl_to_bin bb))
 3. \<And>s' aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (aa, b) \<noteq> Some (a, y) \<longrightarrow> aa = a \<and> b = y \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (a, y) = None proof (prove)
goal (1 subgoal):
 1. \<And>s' aa b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'\<rbrakk> \<Longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (aa, b) \<noteq> Some (a, y) \<longrightarrow> aa = a \<and> b = y \<longrightarrow> map_lift_over transform_cslot_ptr (cdt s') (a, y) = None proof (prove)
goal (2 subgoals):
 1. \<And>s' aa ba ac bc ad bd ae be af bf. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (a, y)) = Some (aa, ba); transform_cslot_ptr (ac, bc) = (a, y); cdt s' (ac, bc) = Some (ad, bd); transform_cslot_ptr (ae, be) = (a, y); cdt s' (ae, be) = Some (af, bf); transform_cslot_ptr (aa, ba) \<noteq> (a, y)\<rbrakk> \<Longrightarrow> False
 2. \<And>s' aa b aaa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (aa, b)) = Some (aaa, ba); cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (a, y)) = Some (ab, bb)\<rbrakk> \<Longrightarrow> (\<forall>a ba. transform_cslot_ptr (a, ba) = (aa, b) \<longrightarrow> (a, ba) \<notin> dom (cdt s')) \<longrightarrow> (\<exists>aa b. transform_cslot_ptr (aa, b) = (a, y) \<and> (aa, b) \<in> dom (cdt s')) \<longrightarrow> aa = a \<longrightarrow> b \<noteq> y proof (prove)
goal (2 subgoals):
 1. \<And>s' aa ba bc ad bd be af bf. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (a, nat (bl_to_bin bc))) = Some (aa, ba); cdt s' (a, bc) = Some (ad, bd); nat (bl_to_bin be) = nat (bl_to_bin bc); cdt s' (a, be) = Some (af, bf); aa = a \<longrightarrow> nat (bl_to_bin ba) \<noteq> nat (bl_to_bin bc); y = nat (bl_to_bin bc)\<rbrakk> \<Longrightarrow> False
 2. \<And>s' aa b aaa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (aa, b)) = Some (aaa, ba); cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (a, y)) = Some (ab, bb)\<rbrakk> \<Longrightarrow> (\<forall>a ba. transform_cslot_ptr (a, ba) = (aa, b) \<longrightarrow> (a, ba) \<notin> dom (cdt s')) \<longrightarrow> (\<exists>aa b. transform_cslot_ptr (aa, b) = (a, y) \<and> (aa, b) \<in> dom (cdt s')) \<longrightarrow> aa = a \<longrightarrow> b \<noteq> y proof (prove)
goal (3 subgoals):
 1. \<And>s' aa ba bc ad bd be af bf. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (a, nat (bl_to_bin bc))) = Some (aa, ba); cdt s' (a, bc) = Some (ad, bd); nat (bl_to_bin be) = nat (bl_to_bin bc); cdt s' (a, be) = Some (af, bf); aa = a \<longrightarrow> nat (bl_to_bin ba) \<noteq> nat (bl_to_bin bc); y = nat (bl_to_bin bc)\<rbrakk> \<Longrightarrow> cdt s' (a, bc) = Some (?slot'241 s' aa ba bc ad bd be af bf)
 2. \<And>s' aa ba bc ad bd be af bf. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (a, nat (bl_to_bin bc))) = Some (aa, ba); cdt s' (a, bc) = Some (ad, bd); nat (bl_to_bin be) = nat (bl_to_bin bc); cdt s' (a, be) = Some (af, bf); aa = a \<longrightarrow> nat (bl_to_bin ba) \<noteq> nat (bl_to_bin bc); y = nat (bl_to_bin bc); cte_wp_at ((\<noteq>) cap.NullCap) (a, bc) s'\<rbrakk> \<Longrightarrow> False
 3. \<And>s' aa b aaa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (aa, b)) = Some (aaa, ba); cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (a, y)) = Some (ab, bb)\<rbrakk> \<Longrightarrow> (\<forall>a ba. transform_cslot_ptr (a, ba) = (aa, b) \<longrightarrow> (a, ba) \<notin> dom (cdt s')) \<longrightarrow> (\<exists>aa b. transform_cslot_ptr (aa, b) = (a, y) \<and> (aa, b) \<in> dom (cdt s')) \<longrightarrow> aa = a \<longrightarrow> b \<noteq> y proof (prove)
goal (2 subgoals):
 1. \<And>s' aa ba bc ad bd be af bf. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (a, nat (bl_to_bin bc))) = Some (aa, ba); cdt s' (a, bc) = Some (ad, bd); nat (bl_to_bin be) = nat (bl_to_bin bc); cdt s' (a, be) = Some (af, bf); aa = a \<longrightarrow> nat (bl_to_bin ba) \<noteq> nat (bl_to_bin bc); y = nat (bl_to_bin bc); cte_wp_at ((\<noteq>) cap.NullCap) (a, bc) s'\<rbrakk> \<Longrightarrow> False
 2. \<And>s' aa b aaa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (aa, b)) = Some (aaa, ba); cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (a, y)) = Some (ab, bb)\<rbrakk> \<Longrightarrow> (\<forall>a ba. transform_cslot_ptr (a, ba) = (aa, b) \<longrightarrow> (a, ba) \<notin> dom (cdt s')) \<longrightarrow> (\<exists>aa b. transform_cslot_ptr (aa, b) = (a, y) \<and> (aa, b) \<in> dom (cdt s')) \<longrightarrow> aa = a \<longrightarrow> b \<noteq> y proof (prove)
goal (3 subgoals):
 1. \<And>s' aa ba bc ad bd be af bf. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (a, nat (bl_to_bin bc))) = Some (aa, ba); cdt s' (a, bc) = Some (ad, bd); nat (bl_to_bin be) = nat (bl_to_bin bc); cdt s' (a, be) = Some (af, bf); aa = a \<longrightarrow> nat (bl_to_bin ba) \<noteq> nat (bl_to_bin bc); y = nat (bl_to_bin bc); cte_wp_at ((\<noteq>) cap.NullCap) (a, bc) s'\<rbrakk> \<Longrightarrow> cte_wp_at (?P244 s' aa ba bc ad bd be af bf) (a, ?ba244 s' aa ba bc ad bd be af bf) s'
 2. \<And>s' aa ba bc ad bd be af bf. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (a, nat (bl_to_bin bc))) = Some (aa, ba); cdt s' (a, bc) = Some (ad, bd); nat (bl_to_bin be) = nat (bl_to_bin bc); cdt s' (a, be) = Some (af, bf); aa = a \<longrightarrow> nat (bl_to_bin ba) \<noteq> nat (bl_to_bin bc); y = nat (bl_to_bin bc); cte_wp_at ((\<noteq>) cap.NullCap) (a, bc) s'; False\<rbrakk> \<Longrightarrow> False
 3. \<And>s' aa b aaa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (aa, b)) = Some (aaa, ba); cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (a, y)) = Some (ab, bb)\<rbrakk> \<Longrightarrow> (\<forall>a ba. transform_cslot_ptr (a, ba) = (aa, b) \<longrightarrow> (a, ba) \<notin> dom (cdt s')) \<longrightarrow> (\<exists>aa b. transform_cslot_ptr (aa, b) = (a, y) \<and> (aa, b) \<in> dom (cdt s')) \<longrightarrow> aa = a \<longrightarrow> b \<noteq> y proof (prove)
goal (1 subgoal):
 1. \<And>s' aa b aaa ba ab bb. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (aa, b)) = Some (aaa, ba); cdt s' (inv_into (dom (cdt s')) transform_cslot_ptr (a, y)) = Some (ab, bb)\<rbrakk> \<Longrightarrow> (\<forall>a ba. transform_cslot_ptr (a, ba) = (aa, b) \<longrightarrow> (a, ba) \<notin> dom (cdt s')) \<longrightarrow> (\<exists>aa b. transform_cslot_ptr (aa, b) = (a, y) \<and> (aa, b) \<in> dom (cdt s')) \<longrightarrow> aa = a \<longrightarrow> b \<noteq> y proof (prove)
goal (1 subgoal):
 1. \<And>s' aa ba bc ac bd. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (a, nat (bl_to_bin bc))) = Some (aa, ba); \<forall>b. nat (bl_to_bin b) = nat (bl_to_bin bc) \<longrightarrow> (a, b) \<notin> dom (cdt s'); y = nat (bl_to_bin bc); cdt s' (a, bc) = Some (ac, bd)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s' aa ba bc ac bd. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (a, nat (bl_to_bin bc))) = Some (aa, ba); \<forall>b. nat (bl_to_bin b) = nat (bl_to_bin bc) \<longrightarrow> (a, b) \<notin> dom (cdt s'); y = nat (bl_to_bin bc); cdt s' (a, bc) = Some (ac, bd)\<rbrakk> \<Longrightarrow> cdt s' (a, bc) = Some (?slot'262 s' aa ba bc ac bd)
 2. \<And>s' aa ba bc ac bd. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (a, nat (bl_to_bin bc))) = Some (aa, ba); \<forall>b. nat (bl_to_bin b) = nat (bl_to_bin bc) \<longrightarrow> (a, b) \<notin> dom (cdt s'); y = nat (bl_to_bin bc); cdt s' (a, bc) = Some (ac, bd); cte_wp_at ((\<noteq>) cap.NullCap) (a, bc) s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s' aa ba bc ac bd. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; typ_at (AArch APageDirectory) a s'; cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (a, nat (bl_to_bin bc))) = Some (aa, ba); \<forall>b. nat (bl_to_bin b) = nat (bl_to_bin bc) \<longrightarrow> (a, b) \<notin> dom (cdt s'); y = nat (bl_to_bin bc); cdt s' (a, bc) = Some (ac, bd); cte_wp_at ((\<noteq>) cap.NullCap) (a, bc) s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s' aa ba bc ac bd. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (a, nat (bl_to_bin bc))) = Some (aa, ba); \<forall>b. nat (bl_to_bin b) = nat (bl_to_bin bc) \<longrightarrow> (a, b) \<notin> dom (cdt s'); y = nat (bl_to_bin bc); cdt s' (a, bc) = Some (ac, bd); cte_wp_at ((\<noteq>) cap.NullCap) (a, bc) s'\<rbrakk> \<Longrightarrow> cte_wp_at (?P265 s' aa ba bc ac bd) (a, ?ba265 s' aa ba bc ac bd) s'
 2. \<And>s' aa ba bc ac bd. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; cdt s' (inv_into (dom (cdt s')) (\<lambda>(a, b). (a, nat (bl_to_bin b))) (a, nat (bl_to_bin bc))) = Some (aa, ba); \<forall>b. nat (bl_to_bin b) = nat (bl_to_bin bc) \<longrightarrow> (a, b) \<notin> dom (cdt s'); y = nat (bl_to_bin bc); cdt s' (a, bc) = Some (ac, bd); cte_wp_at ((\<noteq>) cap.NullCap) (a, bc) s'; False\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!