theory CNode_DR

lemma dcorres_empty_pde_slot:"
ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 \<Longrightarrow> dcorres dc \<top> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)))
  (PageTableUnmap_D.empty_slot (y && ~~ mask pd_bits,unat (y && mask pd_bits >>2)))
  (store_pde y ARM_A.pde.InvalidPDE)" apply (clarsimp simp:store_pde_def get_pd_def get_object_def bind_assoc gets_def) apply (rule dcorres_absorb_get_r) apply (clarsimp simp:assert_def corres_free_fail split:Structures_A.kernel_object.splits arch_kernel_obj.splits) apply (clarsimp simp:PageTableUnmap_D.empty_slot_def) apply (clarsimp simp:set_pd_def set_object_def get_object_def gets_def bind_assoc) apply (rule dcorres_absorb_get_r) apply (clarsimp simp:assert_def corres_free_fail split:Structures_A.kernel_object.splits arch_kernel_obj.splits) apply (simp add:PageTableUnmap_D.empty_slot_def gets_the_def gets_def bind_assoc) apply (rule dcorres_absorb_get_l) apply (clarsimp simp:assert_opt_def opt_cap_pd_Some split:option.splits) apply (intro conjI,clarsimp) apply (clarsimp simp:set_object_def get_def put_def bind_def return_def) apply (clarsimp simp:corres_underlying_def transform_def cur_tcb_def tcb_at_def dest!:get_tcb_SomeD) apply (clarsimp simp:transform_current_thread_def) apply (rule ext) apply (case_tac x) apply (frule(1) arch_obj_not_idle) apply (clarsimp simp: not_idle_thread_def transform_objects_def restrict_map_def map_add_def) apply (rule ext) apply (clarsimp simp: transform_page_directory_contents_def unat_map_def
                         kernel_pde_mask_def ucast_nat_def transform_pde_def
                   split: if_splits ARM_A.pte.split_asm) apply (clarsimp simp:)+ apply (rule corres_dummy_return_pr) apply (rule_tac Q'="\<lambda>r. (=) s'" in  corres_split_forwards'[where r'=dc]) apply (rule corres_guard_imp[OF dummy_remove_cdt_pd_slot]) apply simp+ apply (clarsimp simp:transform_objects_def restrict_map_def) apply (simp add:obj_at_def a_type_def) apply (rule hoare_TrueI) apply wp apply clarsimp apply (clarsimp simp:KHeap_D.set_cap_def gets_the_def gets_def bind_assoc) apply (rule dcorres_absorb_get_l) apply (clarsimp simp:update_slots_def assert_opt_def opt_cap_def slots_of_def
                       opt_object_page_directory has_slots_def object_slots_def
                  split:option.splits) apply (clarsimp simp:KHeap_D.set_object_def set_object_def simpler_modify_def get_def put_def bind_def return_def) apply (clarsimp simp:corres_underlying_def transform_def cur_tcb_def tcb_at_def dest!:get_tcb_SomeD) apply (clarsimp simp:transform_current_thread_def) apply (rule ext) apply (frule(1) arch_obj_not_idle) apply (clarsimp simp: not_idle_thread_def transform_objects_def restrict_map_def map_add_def) apply (subst transform_page_directory_contents_upd[symmetric]) apply (clarsimp simp:transform_pde_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) (PageTableUnmap_D.empty_slot (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2))) (store_pde y InvalidPDE) proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) (PageTableUnmap_D.empty_slot (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2))) (do x <- get;
xa <- assert (\<exists>ya. kheap x (y && ~~ mask pd_bits) = Some ya);
pd <- case the (kheap x (y && ~~ mask pd_bits)) of ArchObj (arch_kernel_obj.PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
set_pd (y && ~~ mask pd_bits) (pd(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; True; (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.empty_slot (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2))) (do x <- assert (\<exists>ya. kheap s' (y && ~~ mask pd_bits) = Some ya);
pd <- case the (kheap s' (y && ~~ mask pd_bits)) of ArchObj (arch_kernel_obj.PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
set_pd (y && ~~ mask pd_bits) (pd(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.empty_slot (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2))) (set_pd (y && ~~ mask pd_bits) (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- KHeap_D.get_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
if cap = cdl_cap.NullCap then return () else do remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od
od) (set_pd (y && ~~ mask pd_bits) (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- KHeap_D.get_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
if cap = cdl_cap.NullCap then return () else do remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od
od) (do x <- get;
ya <- assert (\<exists>ya. kheap x (y && ~~ mask pd_bits) = Some ya);
ya <- assert (a_type (the (kheap x (y && ~~ mask pd_bits))) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))));
s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3 s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do cap <- KHeap_D.get_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
if cap = cdl_cap.NullCap then return () else do remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od
od) (do ya <- assert (\<exists>ya. kheap s'a (y && ~~ mask pd_bits) = Some ya);
ya <- assert (a_type (the (kheap s'a (y && ~~ mask pd_bits))) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))));
s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'a; cur_tcb s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); kheap s'a (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do cap <- KHeap_D.get_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
if cap = cdl_cap.NullCap then return () else do remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'a; cur_tcb s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); kheap s'a (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do x <- get;
cap <- assert_opt (opt_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) x);
if cap = cdl_cap.NullCap then return () else do remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'a; cur_tcb s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); kheap s'a (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform s'a = transform s'; s'a = s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) (transform s'));
if cap = cdl_cap.NullCap then return () else do remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))\<rbrakk> \<Longrightarrow> (transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) = cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od)) \<and> (transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od)) proof (prove)
goal (2 subgoals):
 1. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) = cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od)
 2. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))\<rbrakk> \<Longrightarrow> transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) = cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (\<lambda>s. ({((), s)}, False)) (\<lambda>s. ({((), update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)}, False))
 2. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))\<rbrakk> \<Longrightarrow> transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x3 s' tcb. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) = cdl_cap.NullCap; kheap s' (cur_thread s') = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s') = transform_objects s' \<and> transform_current_thread (update_kheap ((kheap s')(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s') = transform_current_thread s'
 2. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))\<rbrakk> \<Longrightarrow> transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x3 s' tcb. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) = cdl_cap.NullCap; kheap s' (cur_thread s') = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s') = transform_objects s'
 2. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))\<rbrakk> \<Longrightarrow> transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x3 s' tcb x. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) = cdl_cap.NullCap; kheap s' (cur_thread s') = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s') x = transform_objects s' x
 2. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))\<rbrakk> \<Longrightarrow> transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x3 s' tcb x n. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) = cdl_cap.NullCap; kheap s' (cur_thread s') = Some (TCB tcb); x = word_of_nat n; n < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s') x = transform_objects s' x
 2. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))\<rbrakk> \<Longrightarrow> transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x3 s' tcb x n. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) = cdl_cap.NullCap; kheap s' (cur_thread s') = Some (TCB tcb); x = word_of_nat n; n < 2 ^ LENGTH(32); not_idle_thread (y && ~~ mask pd_bits) s'\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s') x = transform_objects s' x
 2. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))\<rbrakk> \<Longrightarrow> transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x3 s' tcb n. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) = cdl_cap.NullCap; kheap s' (cur_thread s') = Some (TCB tcb); n < 4294967296; y && ~~ mask pd_bits \<noteq> idle_thread s'; word_of_nat n = y && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> transform_page_directory_contents (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)) = transform_page_directory_contents x3
 2. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))\<rbrakk> \<Longrightarrow> transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x3 s' tcb n x. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) = cdl_cap.NullCap; kheap s' (cur_thread s') = Some (TCB tcb); n < 4294967296; y && ~~ mask pd_bits \<noteq> idle_thread s'; word_of_nat n = y && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> transform_page_directory_contents (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)) x = transform_page_directory_contents x3 x
 2. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))\<rbrakk> \<Longrightarrow> transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))\<rbrakk> \<Longrightarrow> transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap
od) (do return (?b94 x3 s');
s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (4 subgoals):
 1. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2))) (return (?b94 x3 s'))
 2. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) \<lbrace>?Q96 x3 s'\<rbrace>
 3. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> return (?b94 x3 s') \<lbrace>\<lambda>r. (=) s'\<rbrace>
 4. \<And>x3 s' rv rv'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?Q96 x3 s' rv) ((=) s') (KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap) (K_bind (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) rv') proof (prove)
goal (5 subgoals):
 1. \<And>x3 s' s. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap; transform s' = s\<rbrakk> \<Longrightarrow> True
 2. \<And>x3 s' s. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap; s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and typ_at (AArch APageDirectory) (y && ~~ mask pd_bits)) s
 3. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) \<lbrace>?Q96 x3 s'\<rbrace>
 4. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> return (?b94 x3 s') \<lbrace>\<lambda>r. (=) s'\<rbrace>
 5. \<And>x3 s' rv rv'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?Q96 x3 s' rv) ((=) s') (KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap) (K_bind (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) rv') proof (prove)
goal (4 subgoals):
 1. \<And>x3 s' s. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s; cur_tcb s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); kheap s (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap; s' = s\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) (y && ~~ mask pd_bits) s
 2. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) \<lbrace>?Q96 x3 s'\<rbrace>
 3. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> return (?b94 x3 s') \<lbrace>\<lambda>r. (=) s'\<rbrace>
 4. \<And>x3 s' rv rv'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?Q96 x3 s' rv) ((=) s') (KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap) (K_bind (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) rv') proof (prove)
goal (4 subgoals):
 1. \<And>x3 s. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s; cur_tcb s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); kheap s (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) (y && ~~ mask pd_bits) s
 2. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) \<lbrace>?Q96 x3 s'\<rbrace>
 3. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> return (?b94 x3 s') \<lbrace>\<lambda>r. (=) s'\<rbrace>
 4. \<And>x3 s' rv rv'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?Q96 x3 s' rv) ((=) s') (KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap) (K_bind (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) rv') proof (prove)
goal (3 subgoals):
 1. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> remove_parent (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) \<lbrace>?Q96 x3 s'\<rbrace>
 2. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> return (?b94 x3 s') \<lbrace>\<lambda>r. (=) s'\<rbrace>
 3. \<And>x3 s' rv rv'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?Q96 x3 s' rv) ((=) s') (KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap) (K_bind (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) rv') proof (prove)
goal (2 subgoals):
 1. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> return (?b94 x3 s') \<lbrace>\<lambda>r. (=) s'\<rbrace>
 2. \<And>x3 s' rv rv'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) ((=) s') (KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap) (K_bind (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) rv') proof (prove)
goal (1 subgoal):
 1. \<And>x3 s' rv rv'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) ((=) s') (KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap) (K_bind (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) rv') proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) ((=) s') (KHeap_D.set_cap (y && ~~ mask pd_bits, unat (y && mask pd_bits >> 2)) cdl_cap.NullCap) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) ((=) s') (do x <- get;
obj <- assert_opt (cdl_objects x (y && ~~ mask pd_bits));
ya <- assert (has_slots obj);
(case update_slots ((object_slots obj)(unat (y && mask pd_bits >> 2) \<mapsto> cdl_cap.NullCap)) obj of Tcb t \<Rightarrow> if unat (y && mask pd_bits >> 2) = tcb_ipcbuffer_slot \<and> object_slots obj (unat (y && mask pd_bits >> 2)) \<noteq> Some cdl_cap.NullCap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(unat (y && mask pd_bits >> 2) \<mapsto> cdl_cap.NullCap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(unat (y && mask pd_bits >> 2) \<mapsto> cdl_cap.NullCap)) obj)) >>= KHeap_D.set_object (y && ~~ mask pd_bits)
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s' s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap; True; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do obj <- assert_opt (cdl_objects (transform s'a) (y && ~~ mask pd_bits));
ya <- assert (has_slots obj);
(case update_slots ((object_slots obj)(unat (y && mask pd_bits >> 2) \<mapsto> cdl_cap.NullCap)) obj of Tcb t \<Rightarrow> if unat (y && mask pd_bits >> 2) = tcb_ipcbuffer_slot \<and> object_slots obj (unat (y && mask pd_bits >> 2)) \<noteq> Some cdl_cap.NullCap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(unat (y && mask pd_bits >> 2) \<mapsto> cdl_cap.NullCap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(unat (y && mask pd_bits >> 2) \<mapsto> cdl_cap.NullCap)) obj)) >>= KHeap_D.set_object (y && ~~ mask pd_bits)
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'a; cur_tcb s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); kheap s'a (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (KHeap_D.set_object (y && ~~ mask pd_bits) (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = (transform_page_directory_contents x3)(unat (y && mask pd_bits >> 2) \<mapsto> cdl_cap.NullCap)\<rparr>)) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'a; cur_tcb s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); kheap s'a (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (\<lambda>s. ({((), dupdate_cdl_object (y && ~~ mask pd_bits) (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = (transform_page_directory_contents x3)(unat (y && mask pd_bits >> 2) \<mapsto> cdl_cap.NullCap)\<rparr>) s)}, False)) (\<lambda>s. ({((), update_kheap ((kheap s)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s)}, False)) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a tcb. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); kheap s'a (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap; kheap s'a (cur_thread s'a) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s'a)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s'a) = (transform_objects s'a)(y && ~~ mask pd_bits \<mapsto> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = (transform_page_directory_contents x3)(unat (y && mask pd_bits >> 2) \<mapsto> cdl_cap.NullCap)\<rparr>) \<and> transform_current_thread (update_kheap ((kheap s'a)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s'a) = transform_current_thread s'a proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a tcb. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); kheap s'a (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap; kheap s'a (cur_thread s'a) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s'a)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s'a) = (transform_objects s'a)(y && ~~ mask pd_bits \<mapsto> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = (transform_page_directory_contents x3)(unat (y && mask pd_bits >> 2) \<mapsto> cdl_cap.NullCap)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a tcb x. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); kheap s'a (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap; kheap s'a (cur_thread s'a) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s'a)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s'a) x = ((transform_objects s'a)(y && ~~ mask pd_bits \<mapsto> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = (transform_page_directory_contents x3)(unat (y && mask pd_bits >> 2) \<mapsto> cdl_cap.NullCap)\<rparr>)) x proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a tcb x. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); kheap s'a (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap; kheap s'a (cur_thread s'a) = Some (TCB tcb); not_idle_thread (y && ~~ mask pd_bits) s'a\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s'a)(y && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE))))) s'a) x = ((transform_objects s'a)(y && ~~ mask pd_bits \<mapsto> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = (transform_page_directory_contents x3)(unat (y && mask pd_bits >> 2) \<mapsto> cdl_cap.NullCap)\<rparr>)) x proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a tcb. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); kheap s'a (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap; kheap s'a (cur_thread s'a) = Some (TCB tcb); y && ~~ mask pd_bits \<noteq> idle_thread s'a\<rbrakk> \<Longrightarrow> transform_page_directory_contents (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)) = (transform_page_directory_contents x3)(unat (y && mask pd_bits >> 2) \<mapsto> cdl_cap.NullCap) proof (prove)
goal (2 subgoals):
 1. \<And>x3 s'a tcb. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); kheap s'a (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap; kheap s'a (cur_thread s'a) = Some (TCB tcb); y && ~~ mask pd_bits \<noteq> idle_thread s'a\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 2. \<And>x3 s'a tcb. \<lbrakk>UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); kheap s'a (y && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); a_type (ArchObj (arch_kernel_obj.PageDirectory x3)) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2) := InvalidPDE)))); transform_pde (x3 (UCAST(32 \<rightarrow> 12) (y && mask pd_bits >> 2))) \<noteq> cdl_cap.NullCap; kheap s'a (cur_thread s'a) = Some (TCB tcb); y && ~~ mask pd_bits \<noteq> idle_thread s'a\<rbrakk> \<Longrightarrow> (transform_page_directory_contents x3)(unat (y && mask pd_bits >> 2) \<mapsto> transform_pde InvalidPDE) = (transform_page_directory_contents x3)(unat (y && mask pd_bits >> 2) \<mapsto> cdl_cap.NullCap) proof (prove)
goal:
No subgoals!