theory CNode_DR

lemma dcorres_dummy_empty_slot_pd:
  "\<lbrakk>0xE00 \<le> unat xa ; unat xa < 0x1000\<rbrakk> \<Longrightarrow> dcorres dc \<top> (valid_idle and page_directory_at w)
  (PageTableUnmap_D.empty_slot (w, unat (xa::word32))) (return x)" apply (clarsimp simp:PageTableUnmap_D.empty_slot_def gets_the_def gets_def bind_assoc) apply (rule dcorres_absorb_get_l) apply (clarsimp simp:opt_cap_def slots_of_def) apply  (clarsimp simp:obj_at_def a_type_def
            ,clarsimp split:Structures_A.kernel_object.splits if_splits arch_kernel_obj.splits) apply (subst opt_object_page_directory) apply (simp add:obj_at_def)+ apply (clarsimp simp:assert_opt_def object_slots_def) apply (clarsimp simp:transform_page_directory_contents_def unat_map_def) apply (drule transform_pde_NullCap) apply (simp add:ucast_nat_def)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3584 \<le> unat xa; unat xa < 4096\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and typ_at (AArch APageDirectory) w) (PageTableUnmap_D.empty_slot (w, unat xa)) (return x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3584 \<le> unat xa; unat xa < 4096\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and typ_at (AArch APageDirectory) w) (do x <- get;
cap <- assert_opt (opt_cap (w, unat xa) x);
if cap = cdl_cap.NullCap then return () else do remove_parent (w, unat xa);
KHeap_D.set_cap (w, unat xa) cdl_cap.NullCap
od
od) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>3584 \<le> unat xa; unat xa < 4096; True; (valid_idle and typ_at (AArch APageDirectory) w) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (w, unat xa) (transform s'));
if cap = cdl_cap.NullCap then return () else do remove_parent (w, unat xa);
KHeap_D.set_cap (w, unat xa) cdl_cap.NullCap
od
od) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>3584 \<le> unat xa; unat xa < 4096; valid_idle s'; typ_at (AArch APageDirectory) w s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt ((case cdl_objects (transform s') w of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) (unat xa));
if cap = cdl_cap.NullCap then return () else do remove_parent (w, unat xa);
KHeap_D.set_cap (w, unat xa) cdl_cap.NullCap
od
od) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3. \<lbrakk>3584 \<le> unat xa; unat xa < 4096; valid_idle s'; kheap s' w = Some (ArchObj (arch_kernel_obj.PageDirectory x3))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt ((case cdl_objects (transform s') w of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) (unat xa));
if cap = cdl_cap.NullCap then return () else do remove_parent (w, unat xa);
KHeap_D.set_cap (w, unat xa) cdl_cap.NullCap
od
od) (return x) proof (prove)
goal (3 subgoals):
 1. \<And>s' x3. \<lbrakk>3584 \<le> unat xa; unat xa < 4096; valid_idle s'; kheap s' w = Some (ArchObj (arch_kernel_obj.PageDirectory x3))\<rbrakk> \<Longrightarrow> valid_idle s'
 2. \<And>s' x3. \<lbrakk>3584 \<le> unat xa; unat xa < 4096; valid_idle s'; kheap s' w = Some (ArchObj (arch_kernel_obj.PageDirectory x3))\<rbrakk> \<Longrightarrow> kheap s' w = Some (ArchObj (arch_kernel_obj.PageDirectory (?fun77 s' x3)))
 3. \<And>s' x3. \<lbrakk>3584 \<le> unat xa; unat xa < 4096; valid_idle s'; kheap s' w = Some (ArchObj (arch_kernel_obj.PageDirectory x3))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt ((case Some (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents (?fun77 s' x3)\<rparr>) of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) (unat xa));
if cap = cdl_cap.NullCap then return () else do remove_parent (w, unat xa);
KHeap_D.set_cap (w, unat xa) cdl_cap.NullCap
od
od) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3. \<lbrakk>3584 \<le> unat xa; unat xa < 4096; valid_idle s'; kheap s' w = Some (ArchObj (arch_kernel_obj.PageDirectory x3))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (object_slots (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents x3\<rparr>) (unat xa));
if cap = cdl_cap.NullCap then return () else do remove_parent (w, unat xa);
KHeap_D.set_cap (w, unat xa) cdl_cap.NullCap
od
od) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3. \<lbrakk>3584 \<le> unat xa; unat xa < 4096; valid_idle s'; kheap s' w = Some (ArchObj (arch_kernel_obj.PageDirectory x3))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- case transform_page_directory_contents x3 (unat xa) of None \<Rightarrow> fail | Some v \<Rightarrow> return v;
if cap = cdl_cap.NullCap then return () else do remove_parent (w, unat xa);
KHeap_D.set_cap (w, unat xa) cdl_cap.NullCap
od
od) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3. \<lbrakk>3584 \<le> unat xa; unat xa < 4096; valid_idle s'; kheap s' w = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); transform_pde (kernel_pde_mask x3 (UCAST(32 \<rightarrow> 12) xa)) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- remove_parent (w, unat xa);
KHeap_D.set_cap (w, unat xa) cdl_cap.NullCap
od) (return x) proof (prove)
goal (2 subgoals):
 1. \<And>s' x3. \<lbrakk>unat xa < 4096; valid_idle s'; kheap s' w = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); transform_pde (kernel_pde_mask x3 (UCAST(32 \<rightarrow> 12) xa)) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> unat xa < 4096
 2. \<And>s' x3. \<lbrakk>unat xa < 4096; valid_idle s'; kheap s' w = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); transform_pde (kernel_pde_mask x3 (UCAST(32 \<rightarrow> 12) xa)) \<noteq> cdl_cap.NullCap; transform_pde (kernel_pde_mask (?ptx84 s' x3) (UCAST(32 \<rightarrow> 12) xa)) = cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- remove_parent (w, unat xa);
KHeap_D.set_cap (w, unat xa) cdl_cap.NullCap
od) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3. \<lbrakk>unat xa < 4096; valid_idle s'; kheap s' w = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); transform_pde (kernel_pde_mask x3 (UCAST(32 \<rightarrow> 12) xa)) \<noteq> cdl_cap.NullCap; transform_pde (kernel_pde_mask (?ptx84 s' x3) (UCAST(32 \<rightarrow> 12) xa)) = cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- remove_parent (w, unat xa);
KHeap_D.set_cap (w, unat xa) cdl_cap.NullCap
od) (return x) proof (prove)
goal:
No subgoals!