theory CNode_DR

lemma dcorres_empty_pte_slot:
  " 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 pt_bits, unat (y && mask pt_bits >> 2)))
     (store_pte y ARM_A.pte.InvalidPTE)" apply (clarsimp simp:store_pte_def get_pt_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_pt_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_pt_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_table_contents_def unat_map_def transform_pte_def ucast_nat_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_pt_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_table
                       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_table_contents_upd[symmetric]) apply (clarsimp simp:transform_pte_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 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 pt_bits, unat (y && mask pt_bits >> 2))) (store_pte y InvalidPTE) proof (prove)
goal (1 subgoal):
 1. 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 pt_bits, unat (y && mask pt_bits >> 2))) (do x <- get;
xa <- assert (\<exists>ya. kheap x (y && ~~ mask pt_bits) = Some ya);
pt <- case the (kheap x (y && ~~ mask pt_bits)) of ArchObj (arch_kernel_obj.PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
set_pt (y && ~~ mask pt_bits) (pt(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>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 pt_bits, unat (y && mask pt_bits >> 2))) (do x <- assert (\<exists>ya. kheap s' (y && ~~ mask pt_bits) = Some ya);
pt <- case the (kheap s' (y && ~~ mask pt_bits)) of ArchObj (arch_kernel_obj.PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
set_pt (y && ~~ mask pt_bits) (pt(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' x2. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (PageTableUnmap_D.empty_slot (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2))) (set_pt (y && ~~ mask pt_bits) (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))) proof (prove)
goal (1 subgoal):
 1. \<And>s' x2. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- KHeap_D.get_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
if cap = cdl_cap.NullCap then return () else do remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od
od) (set_pt (y && ~~ mask pt_bits) (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))) proof (prove)
goal (1 subgoal):
 1. \<And>s' x2. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- KHeap_D.get_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
if cap = cdl_cap.NullCap then return () else do remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od
od) (do x <- get;
ya <- assert (\<exists>ya. kheap x (y && ~~ mask pt_bits) = Some ya);
ya <- assert (a_type (the (kheap x (y && ~~ mask pt_bits))) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))));
s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' x2 s'a. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); 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 pt_bits, unat (y && mask pt_bits >> 2));
if cap = cdl_cap.NullCap then return () else do remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od
od) (do ya <- assert (\<exists>ya. kheap s'a (y && ~~ mask pt_bits) = Some ya);
ya <- assert (a_type (the (kheap s'a (y && ~~ mask pt_bits))) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))));
s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s'a. \<lbrakk>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 pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do cap <- KHeap_D.get_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
if cap = cdl_cap.NullCap then return () else do remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s'a. \<lbrakk>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 pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do x <- get;
cap <- assert_opt (opt_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) x);
if cap = cdl_cap.NullCap then return () else do remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s'a s'. \<lbrakk>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 pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform s'a = transform s'; s'a = s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do cap <- assert_opt (opt_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) (transform s'));
if cap = cdl_cap.NullCap then return () else do remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))\<rbrakk> \<Longrightarrow> (transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) = cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od)) \<and> (transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od)) proof (prove)
goal (2 subgoals):
 1. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) = cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return ()) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od)
 2. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))\<rbrakk> \<Longrightarrow> transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) = cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (\<lambda>s. ({((), s)}, False)) (\<lambda>s. ({((), update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)}, False))
 2. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))\<rbrakk> \<Longrightarrow> transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x2 s' tcb. \<lbrakk>valid_idle s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) = cdl_cap.NullCap; kheap s' (cur_thread s') = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s') = transform_objects s' \<and> transform_current_thread (update_kheap ((kheap s')(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s') = transform_current_thread s'
 2. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))\<rbrakk> \<Longrightarrow> transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x2 s' tcb. \<lbrakk>valid_idle s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) = cdl_cap.NullCap; kheap s' (cur_thread s') = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s') = transform_objects s'
 2. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))\<rbrakk> \<Longrightarrow> transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x2 s' tcb x. \<lbrakk>valid_idle s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) = cdl_cap.NullCap; kheap s' (cur_thread s') = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s') x = transform_objects s' x
 2. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))\<rbrakk> \<Longrightarrow> transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x2 s' tcb x n. \<lbrakk>valid_idle s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_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 pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s') x = transform_objects s' x
 2. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))\<rbrakk> \<Longrightarrow> transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x2 s' tcb x n. \<lbrakk>valid_idle s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_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 pt_bits) s'\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s') x = transform_objects s' x
 2. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))\<rbrakk> \<Longrightarrow> transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x2 s' tcb n. \<lbrakk>valid_idle s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) = cdl_cap.NullCap; kheap s' (cur_thread s') = Some (TCB tcb); n < 4294967296; y && ~~ mask pt_bits \<noteq> idle_thread s'; word_of_nat n = y && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> transform_page_table_contents (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)) = transform_page_table_contents x2
 2. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))\<rbrakk> \<Longrightarrow> transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x2 s' tcb n x. \<lbrakk>valid_idle s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) = cdl_cap.NullCap; kheap s' (cur_thread s') = Some (TCB tcb); n < 4294967296; y && ~~ mask pt_bits \<noteq> idle_thread s'; word_of_nat n = y && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> transform_page_table_contents (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)) x = transform_page_table_contents x2 x
 2. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))\<rbrakk> \<Longrightarrow> transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))\<rbrakk> \<Longrightarrow> transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do ya <- remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2));
KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap
od) (do return (?b90 x2 s');
s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (4 subgoals):
 1. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2))) (return (?b90 x2 s'))
 2. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) \<lbrace>?Q92 x2 s'\<rbrace>
 3. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> return (?b90 x2 s') \<lbrace>\<lambda>r. (=) s'\<rbrace>
 4. \<And>x2 s' rv rv'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?Q92 x2 s' rv) ((=) s') (KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap) (K_bind (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) rv') proof (prove)
goal (5 subgoals):
 1. \<And>x2 s' s. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap; transform s' = s\<rbrakk> \<Longrightarrow> True
 2. \<And>x2 s' s. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_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 APageTable) (y && ~~ mask pt_bits)) s
 3. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) \<lbrace>?Q92 x2 s'\<rbrace>
 4. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> return (?b90 x2 s') \<lbrace>\<lambda>r. (=) s'\<rbrace>
 5. \<And>x2 s' rv rv'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?Q92 x2 s' rv) ((=) s') (KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap) (K_bind (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) rv') proof (prove)
goal (4 subgoals):
 1. \<And>x2 s' s. \<lbrakk>valid_idle s; cur_tcb s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); kheap s (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap; s' = s\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) (y && ~~ mask pt_bits) s
 2. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) \<lbrace>?Q92 x2 s'\<rbrace>
 3. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> return (?b90 x2 s') \<lbrace>\<lambda>r. (=) s'\<rbrace>
 4. \<And>x2 s' rv rv'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?Q92 x2 s' rv) ((=) s') (KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap) (K_bind (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) rv') proof (prove)
goal (4 subgoals):
 1. \<And>x2 s. \<lbrakk>valid_idle s; cur_tcb s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); kheap s (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) (y && ~~ mask pt_bits) s
 2. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) \<lbrace>?Q92 x2 s'\<rbrace>
 3. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> return (?b90 x2 s') \<lbrace>\<lambda>r. (=) s'\<rbrace>
 4. \<And>x2 s' rv rv'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?Q92 x2 s' rv) ((=) s') (KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap) (K_bind (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) rv') proof (prove)
goal (3 subgoals):
 1. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> remove_parent (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) \<lbrace>?Q92 x2 s'\<rbrace>
 2. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> return (?b90 x2 s') \<lbrace>\<lambda>r. (=) s'\<rbrace>
 3. \<And>x2 s' rv rv'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?Q92 x2 s' rv) ((=) s') (KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap) (K_bind (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) rv') proof (prove)
goal (2 subgoals):
 1. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> return (?b90 x2 s') \<lbrace>\<lambda>r. (=) s'\<rbrace>
 2. \<And>x2 s' rv rv'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) ((=) s') (KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap) (K_bind (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) rv') proof (prove)
goal (1 subgoal):
 1. \<And>x2 s' rv rv'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) ((=) s') (KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap) (K_bind (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) rv') proof (prove)
goal (1 subgoal):
 1. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) ((=) s') (KHeap_D.set_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) cdl_cap.NullCap) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s'. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) ((=) s') (do x <- get;
obj <- assert_opt (cdl_objects x (y && ~~ mask pt_bits));
ya <- assert (has_slots obj);
(case update_slots ((object_slots obj)(unat (y && mask pt_bits >> 2) \<mapsto> cdl_cap.NullCap)) obj of Tcb t \<Rightarrow> if unat (y && mask pt_bits >> 2) = tcb_ipcbuffer_slot \<and> object_slots obj (unat (y && mask pt_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 pt_bits >> 2) \<mapsto> cdl_cap.NullCap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(unat (y && mask pt_bits >> 2) \<mapsto> cdl_cap.NullCap)) obj)) >>= KHeap_D.set_object (y && ~~ mask pt_bits)
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s' s'a. \<lbrakk>valid_idle s'; cur_tcb s'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s') (cdt s'); kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_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 pt_bits));
ya <- assert (has_slots obj);
(case update_slots ((object_slots obj)(unat (y && mask pt_bits >> 2) \<mapsto> cdl_cap.NullCap)) obj of Tcb t \<Rightarrow> if unat (y && mask pt_bits >> 2) = tcb_ipcbuffer_slot \<and> object_slots obj (unat (y && mask pt_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 pt_bits >> 2) \<mapsto> cdl_cap.NullCap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(unat (y && mask pt_bits >> 2) \<mapsto> cdl_cap.NullCap)) obj)) >>= KHeap_D.set_object (y && ~~ mask pt_bits)
od) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s'a. \<lbrakk>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 pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (KHeap_D.set_object (y && ~~ mask pt_bits) (cdl_object.PageTable \<lparr>cdl_page_table_caps = (transform_page_table_contents x2)(unat (y && mask pt_bits >> 2) \<mapsto> cdl_cap.NullCap)\<rparr>)) (do s <- get;
put (update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s'a. \<lbrakk>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 pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (\<lambda>s. ({((), dupdate_cdl_object (y && ~~ mask pt_bits) (cdl_object.PageTable \<lparr>cdl_page_table_caps = (transform_page_table_contents x2)(unat (y && mask pt_bits >> 2) \<mapsto> cdl_cap.NullCap)\<rparr>) s)}, False)) (\<lambda>s. ({((), update_kheap ((kheap s)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s)}, False)) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s'a tcb. \<lbrakk>valid_idle s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); kheap s'a (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_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 pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s'a) = (transform_objects s'a)(y && ~~ mask pt_bits \<mapsto> cdl_object.PageTable \<lparr>cdl_page_table_caps = (transform_page_table_contents x2)(unat (y && mask pt_bits >> 2) \<mapsto> cdl_cap.NullCap)\<rparr>) \<and> transform_current_thread (update_kheap ((kheap s'a)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s'a) = transform_current_thread s'a proof (prove)
goal (1 subgoal):
 1. \<And>x2 s'a tcb. \<lbrakk>valid_idle s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); kheap s'a (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_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 pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s'a) = (transform_objects s'a)(y && ~~ mask pt_bits \<mapsto> cdl_object.PageTable \<lparr>cdl_page_table_caps = (transform_page_table_contents x2)(unat (y && mask pt_bits >> 2) \<mapsto> cdl_cap.NullCap)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s'a tcb x. \<lbrakk>valid_idle s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); kheap s'a (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_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 pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s'a) x = ((transform_objects s'a)(y && ~~ mask pt_bits \<mapsto> cdl_object.PageTable \<lparr>cdl_page_table_caps = (transform_page_table_contents x2)(unat (y && mask pt_bits >> 2) \<mapsto> cdl_cap.NullCap)\<rparr>)) x proof (prove)
goal (1 subgoal):
 1. \<And>x2 s'a tcb x. \<lbrakk>valid_idle s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); kheap s'a (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap; kheap s'a (cur_thread s'a) = Some (TCB tcb); not_idle_thread (y && ~~ mask pt_bits) s'a\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s'a)(y && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE))))) s'a) x = ((transform_objects s'a)(y && ~~ mask pt_bits \<mapsto> cdl_object.PageTable \<lparr>cdl_page_table_caps = (transform_page_table_contents x2)(unat (y && mask pt_bits >> 2) \<mapsto> cdl_cap.NullCap)\<rparr>)) x proof (prove)
goal (1 subgoal):
 1. \<And>x2 s'a tcb. \<lbrakk>valid_idle s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); kheap s'a (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap; kheap s'a (cur_thread s'a) = Some (TCB tcb); y && ~~ mask pt_bits \<noteq> idle_thread s'a\<rbrakk> \<Longrightarrow> transform_page_table_contents (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)) = (transform_page_table_contents x2)(unat (y && mask pt_bits >> 2) \<mapsto> cdl_cap.NullCap) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s'a tcb. \<lbrakk>valid_idle s'a; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s'a) (cdt s'a); kheap s'a (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); a_type (ArchObj (arch_kernel_obj.PageTable x2)) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := InvalidPTE)))); transform_pte (x2 (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) \<noteq> cdl_cap.NullCap; kheap s'a (cur_thread s'a) = Some (TCB tcb); y && ~~ mask pt_bits \<noteq> idle_thread s'a\<rbrakk> \<Longrightarrow> (transform_page_table_contents x2)(unat (y && mask pt_bits >> 2) \<mapsto> transform_pte InvalidPTE) = (transform_page_table_contents x2)(unat (y && mask pt_bits >> 2) \<mapsto> cdl_cap.NullCap) proof (prove)
goal:
No subgoals!