theory Finalise_DR

lemma dcorres_delete_cap_simple_set_pde:
  " ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots
    \<Longrightarrow>dcorres dc \<top> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))
    and (pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr
         or pd_section_relation (ptr && ~~ mask pd_bits) oid ptr
         or pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr)
    and valid_idle and ko_at (ArchObj (arch_kernel_obj.PageDirectory fun)) (ptr && ~~ mask pd_bits))
             (delete_cap_simple (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)))
             (set_pd (ptr && ~~ mask pd_bits) (fun(ucast (ptr && mask pd_bits >> 2) := ARM_A.pde.InvalidPDE)))" apply (simp add: delete_cap_simple_def set_pd_def gets_the_def gets_def bind_assoc) apply (rule dcorres_absorb_get_l) apply (clarsimp simp: assert_def corres_free_fail
                 split: Structures_A.kernel_object.split_asm arch_kernel_obj.splits) apply (erule disjE) apply (frule opt_cap_page_table, simp+) apply (clarsimp simp: gets_def assert_opt_def PageTableUnmap_D.is_final_cap_def PageTableUnmap_D.is_final_cap'_def) apply (rule dcorres_absorb_get_l) apply (clarsimp simp: always_empty_slot_def gets_the_def gets_def bind_assoc) apply (rule remove_cdt_pd_slot_exec) apply (rule corres_guard_imp) apply (rule dcorres_set_pde_cap) apply (simp add: transform_pte_def)+ apply (clarsimp simp: pd_pt_relation_def transform_pde_def)+ apply (rule page_directory_at_rev) apply simp apply (frule opt_cap_section,simp+) apply (clarsimp simp: gets_def assert_opt_def PageTableUnmap_D.is_final_cap_def PageTableUnmap_D.is_final_cap'_def) apply (rule dcorres_absorb_get_l) apply (clarsimp simp: always_empty_slot_def gets_the_def gets_def bind_assoc) apply (rule remove_cdt_pd_slot_exec) apply (rule corres_guard_imp) apply (rule dcorres_set_pde_cap) apply simp+ apply (clarsimp simp: pd_pt_relation_def transform_pde_def obj_at_def a_type_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and (pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr or pd_section_relation (ptr && ~~ mask pd_bits) oid ptr or pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr) and valid_idle and ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits)) (delete_cap_simple (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))) (set_pd (ptr && ~~ mask pd_bits) (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))) proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and (pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr or pd_section_relation (ptr && ~~ mask pd_bits) oid ptr or pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr) and valid_idle and ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits)) (do x <- get;
cap <- assert_opt (opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) x);
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; True; ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and (pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr or pd_section_relation (ptr && ~~ mask pd_bits) oid ptr or pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr) and valid_idle and ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits)) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s' \<or> pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s' \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'; valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE)))))
 2. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s' \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s') = Some (cdl_cap.PageTableCap oid Fake None)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do final <- PageTableUnmap_D.is_final_cap (cdl_cap.PageTableCap oid Fake None);
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE)))))
 2. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s' \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s') = Some (cdl_cap.PageTableCap oid Fake None)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE)))))
 2. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s' \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (2 subgoals):
 1. \<And>s' s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s') = Some (cdl_cap.PageTableCap oid Fake None); transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE)))))
 2. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s' \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (2 subgoals):
 1. \<And>s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (cdl_cap.PageTableCap oid Fake None)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- remove_parent (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2));
KHeap_D.set_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) cdl_cap.NullCap
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE)))))
 2. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s' \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (3 subgoals):
 1. \<And>s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (cdl_cap.PageTableCap oid Fake None)\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) ((=) s'a) (KHeap_D.set_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) cdl_cap.NullCap) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE)))))
 2. \<And>s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (cdl_cap.PageTableCap oid Fake None)\<rbrakk> \<Longrightarrow> s'a = s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) (ptr && ~~ mask pd_bits)) s
 3. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s' \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (5 subgoals):
 1. \<And>s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (cdl_cap.PageTableCap oid Fake None)\<rbrakk> \<Longrightarrow> dcorres dc (?Q22 s'a) (?Q'22 s'a) (KHeap_D.set_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) cdl_cap.NullCap) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE)))))
 2. \<And>s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (cdl_cap.PageTableCap oid Fake None); True\<rbrakk> \<Longrightarrow> ?Q22 s'a s
 3. \<And>s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (cdl_cap.PageTableCap oid Fake None); s'a = s\<rbrakk> \<Longrightarrow> ?Q'22 s'a s
 4. \<And>s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (cdl_cap.PageTableCap oid Fake None)\<rbrakk> \<Longrightarrow> s'a = s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) (ptr && ~~ mask pd_bits)) s
 5. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s' \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (7 subgoals):
 1. \<And>s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (cdl_cap.PageTableCap oid Fake None)\<rbrakk> \<Longrightarrow> ptr && mask pd_bits >> 2 = ?ptr26 s'a && mask pd_bits >> 2
 2. \<And>s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (cdl_cap.PageTableCap oid Fake None)\<rbrakk> \<Longrightarrow> cdl_cap.NullCap = transform_pde InvalidPDE
 3. \<And>s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (cdl_cap.PageTableCap oid Fake None)\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (?ptr26 s'a && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 4. \<And>s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (cdl_cap.PageTableCap oid Fake None); True\<rbrakk> \<Longrightarrow> True
 5. \<And>s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (cdl_cap.PageTableCap oid Fake None); s'a = s\<rbrakk> \<Longrightarrow> (valid_idle and ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits)) s
 6. \<And>s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (cdl_cap.PageTableCap oid Fake None)\<rbrakk> \<Longrightarrow> s'a = s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) (ptr && ~~ mask pd_bits)) s
 7. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s' \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (6 subgoals):
 1. \<And>s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (cdl_cap.PageTableCap oid Fake None)\<rbrakk> \<Longrightarrow> cdl_cap.NullCap = transform_pde InvalidPDE
 2. \<And>s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (cdl_cap.PageTableCap oid Fake None)\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 3. \<And>s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (cdl_cap.PageTableCap oid Fake None); True\<rbrakk> \<Longrightarrow> True
 4. \<And>s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (cdl_cap.PageTableCap oid Fake None); s'a = s\<rbrakk> \<Longrightarrow> (valid_idle and ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits)) s
 5. \<And>s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (cdl_cap.PageTableCap oid Fake None)\<rbrakk> \<Longrightarrow> s'a = s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) (ptr && ~~ mask pd_bits)) s
 6. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s' \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (2 subgoals):
 1. \<And>s funa u v ref. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); valid_idle s; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s) = Some (cdl_cap.PageTableCap (ptrFromPAddr ref) Fake None); kheap s (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory funa)); typ_at (AArch APageTable) (ptrFromPAddr ref) s; funa (UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2)) = PageTablePDE ref u v; oid = ptrFromPAddr ref\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) (ptr && ~~ mask pd_bits) s
 2. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s' \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (2 subgoals):
 1. \<And>s funa u v ref. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); valid_idle s; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s) = Some (cdl_cap.PageTableCap (ptrFromPAddr ref) Fake None); kheap s (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory funa)); typ_at (AArch APageTable) (ptrFromPAddr ref) s; funa (UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2)) = PageTablePDE ref u v; oid = ptrFromPAddr ref\<rbrakk> \<Longrightarrow> kheap s (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory (?fun46 s funa u v ref)))
 2. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s' \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s' \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s' \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'; \<exists>f sz. opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s') = Some (FrameCap False oid f sz Fake None)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'));
unless (cap = cdl_cap.NullCap) (do final <- PageTableUnmap_D.is_final_cap cap;
y <- PageTableUnmap_D.fast_finalise cap final;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od)
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (1 subgoal):
 1. \<And>s' f sz. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s' \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s') = Some (FrameCap False oid f sz Fake None)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do s <- get;
always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (1 subgoal):
 1. \<And>s' f sz s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); valid_idle s'; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s' \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s') = Some (FrameCap False oid f sz Fake None); transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (always_empty_slot (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (1 subgoal):
 1. \<And>f sz s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (FrameCap False oid f sz Fake None)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do y <- remove_parent (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2));
KHeap_D.set_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) cdl_cap.NullCap
od) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE))))) proof (prove)
goal (2 subgoals):
 1. \<And>f sz s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (FrameCap False oid f sz Fake None)\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) ((=) s'a) (KHeap_D.set_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) cdl_cap.NullCap) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE)))))
 2. \<And>f sz s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (FrameCap False oid f sz Fake None)\<rbrakk> \<Longrightarrow> s'a = s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) (ptr && ~~ mask pd_bits)) s proof (prove)
goal (4 subgoals):
 1. \<And>f sz s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (FrameCap False oid f sz Fake None)\<rbrakk> \<Longrightarrow> dcorres dc (?Q61 f sz s'a) (?Q'61 f sz s'a) (KHeap_D.set_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) cdl_cap.NullCap) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (fun(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := InvalidPDE)))))
 2. \<And>f sz s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (FrameCap False oid f sz Fake None); True\<rbrakk> \<Longrightarrow> ?Q61 f sz s'a s
 3. \<And>f sz s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (FrameCap False oid f sz Fake None); s'a = s\<rbrakk> \<Longrightarrow> ?Q'61 f sz s'a s
 4. \<And>f sz s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (FrameCap False oid f sz Fake None)\<rbrakk> \<Longrightarrow> s'a = s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) (ptr && ~~ mask pd_bits)) s proof (prove)
goal (6 subgoals):
 1. \<And>f sz s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (FrameCap False oid f sz Fake None)\<rbrakk> \<Longrightarrow> ptr && mask pd_bits >> 2 = ?ptr65 f sz s'a && mask pd_bits >> 2
 2. \<And>f sz s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (FrameCap False oid f sz Fake None)\<rbrakk> \<Longrightarrow> cdl_cap.NullCap = transform_pde InvalidPDE
 3. \<And>f sz s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (FrameCap False oid f sz Fake None)\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (?ptr65 f sz s'a && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 4. \<And>f sz s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (FrameCap False oid f sz Fake None); True\<rbrakk> \<Longrightarrow> True
 5. \<And>f sz s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (FrameCap False oid f sz Fake None); s'a = s\<rbrakk> \<Longrightarrow> (valid_idle and ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits)) s
 6. \<And>f sz s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (FrameCap False oid f sz Fake None)\<rbrakk> \<Longrightarrow> s'a = s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) (ptr && ~~ mask pd_bits)) s proof (prove)
goal (5 subgoals):
 1. \<And>f sz s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (FrameCap False oid f sz Fake None)\<rbrakk> \<Longrightarrow> cdl_cap.NullCap = transform_pde InvalidPDE
 2. \<And>f sz s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (FrameCap False oid f sz Fake None)\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 3. \<And>f sz s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (FrameCap False oid f sz Fake None); True\<rbrakk> \<Longrightarrow> True
 4. \<And>f sz s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (FrameCap False oid f sz Fake None); s'a = s\<rbrakk> \<Longrightarrow> (valid_idle and ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits)) s
 5. \<And>f sz s'a s. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory fun) (ptr && ~~ mask pd_bits) s'a; pd_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a \<or> pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr s'a; opt_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform s'a) = Some (FrameCap False oid f sz Fake None)\<rbrakk> \<Longrightarrow> s'a = s \<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) (ptr && ~~ mask pd_bits)) s proof (prove)
goal:
No subgoals!