theory CNode_DR

lemma store_pde_set_cap_corres:
  "\<lbrakk>ucast (ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots \<rbrakk> \<Longrightarrow>
   dcorres dc \<top> valid_idle (return a)
      (store_pde ptr pde)" apply (clarsimp simp:store_pde_def get_pd_def set_pd_def set_object_def get_object_def gets_def bind_assoc) apply (rule dcorres_absorb_get_r) apply (clarsimp simp:corres_free_fail assert_def split:Structures_A.kernel_object.splits arch_kernel_obj.splits) apply (rule dcorres_absorb_get_r) apply (clarsimp simp:corres_free_fail) apply (frule arch_obj_not_idle) apply simp apply (simp add:not_idle_thread_def) apply (clarsimp simp:set_object_def return_def get_def put_def corres_underlying_def bind_def) apply (simp add:transform_def transform_current_thread_def) apply (rule ext) apply (clarsimp simp: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 ) apply (simp add:kernel_mapping_slots_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots \<Longrightarrow> dcorres dc (\<lambda>_. True) valid_idle (return a) (store_pde ptr pde) proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots \<Longrightarrow> dcorres dc (\<lambda>_. True) valid_idle (return a) (do x <- get;
xa <- assert (\<exists>y. kheap x (ptr && ~~ mask pd_bits) = Some y);
pd <- case the (kheap x (ptr && ~~ mask pd_bits)) of ArchObj (arch_kernel_obj.PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
x <- get;
y <- assert (\<exists>y. kheap x (ptr && ~~ mask pd_bits) = Some y);
y <- assert (a_type (the (kheap x (ptr && ~~ mask pd_bits))) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pd(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde)))));
s <- get;
put (update_kheap ((kheap s)(ptr && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (pd(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; True; valid_idle s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return a) (do x <- assert (\<exists>y. kheap s' (ptr && ~~ mask pd_bits) = Some y);
pd <- case the (kheap s' (ptr && ~~ mask pd_bits)) of ArchObj (arch_kernel_obj.PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
x <- get;
y <- assert (\<exists>y. kheap x (ptr && ~~ mask pd_bits) = Some y);
y <- assert (a_type (the (kheap x (ptr && ~~ mask pd_bits))) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pd(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde)))));
s <- get;
put (update_kheap ((kheap s)(ptr && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (pd(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_idle s'; kheap s' (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return a) (do x <- get;
y <- if \<exists>y. kheap x (ptr && ~~ mask pd_bits) = Some y then return () else fail;
y <- if a_type (the (kheap x (ptr && ~~ mask pd_bits))) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde)))) then return () else fail;
s <- get;
put (update_kheap ((kheap s)(ptr && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3 s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_idle s'; kheap s' (ptr && ~~ 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) (return a) (do y <- if \<exists>y. kheap s'a (ptr && ~~ mask pd_bits) = Some y then return () else fail;
y <- if a_type (the (kheap s'a (ptr && ~~ mask pd_bits))) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde)))) then return () else fail;
s <- get;
put (update_kheap ((kheap s)(ptr && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_idle s'a; kheap s'a (ptr && ~~ 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) (ptr && mask pd_bits >> 2) := pde))))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (return a) (do s <- get;
put (update_kheap ((kheap s)(ptr && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde))))) s)
od) proof (prove)
goal (2 subgoals):
 1. \<And>x3 s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_idle s'a; kheap s'a (ptr && ~~ 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) (ptr && mask pd_bits >> 2) := pde))))\<rbrakk> \<Longrightarrow> kheap s'a (?ptr32 x3 s'a) = Some (ArchObj (?x32 x3 s'a))
 2. \<And>x3 s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_idle s'a; kheap s'a (ptr && ~~ 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) (ptr && mask pd_bits >> 2) := pde)))); not_idle_thread (?ptr32 x3 s'a) s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (return a) (do s <- get;
put (update_kheap ((kheap s)(ptr && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_idle s'a; kheap s'a (ptr && ~~ 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) (ptr && mask pd_bits >> 2) := pde)))); not_idle_thread (ptr && ~~ mask pd_bits) s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (return a) (do s <- get;
put (update_kheap ((kheap s)(ptr && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_idle s'a; kheap s'a (ptr && ~~ 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) (ptr && mask pd_bits >> 2) := pde)))); ptr && ~~ mask pd_bits \<noteq> idle_thread s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (return a) (do s <- get;
put (update_kheap ((kheap s)(ptr && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_idle s'a; kheap s'a (ptr && ~~ 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) (ptr && mask pd_bits >> 2) := pde)))); ptr && ~~ mask pd_bits \<noteq> idle_thread s'a\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap s'a)(ptr && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde))))) s'a) = transform s'a proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_idle s'a; kheap s'a (ptr && ~~ 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) (ptr && mask pd_bits >> 2) := pde)))); ptr && ~~ mask pd_bits \<noteq> idle_thread s'a\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s'a)(ptr && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde))))) s'a) = transform_objects s'a proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a x. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_idle s'a; kheap s'a (ptr && ~~ 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) (ptr && mask pd_bits >> 2) := pde)))); ptr && ~~ mask pd_bits \<noteq> idle_thread s'a\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s'a)(ptr && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde))))) s'a) x = transform_objects s'a x proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_idle s'a; kheap s'a (ptr && ~~ 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) (ptr && mask pd_bits >> 2) := pde)))); ptr && ~~ mask pd_bits \<noteq> idle_thread s'a\<rbrakk> \<Longrightarrow> transform_page_directory_contents (x3(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde)) = transform_page_directory_contents x3 proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a x. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_idle s'a; kheap s'a (ptr && ~~ 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) (ptr && mask pd_bits >> 2) := pde)))); ptr && ~~ mask pd_bits \<noteq> idle_thread s'a\<rbrakk> \<Longrightarrow> transform_page_directory_contents (x3(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde)) x = transform_page_directory_contents x3 x proof (prove)
goal (1 subgoal):
 1. \<And>x3 s'a x. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_idle s'a; kheap s'a (ptr && ~~ 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) (ptr && mask pd_bits >> 2) := pde)))); ptr && ~~ mask pd_bits \<noteq> idle_thread s'a; word_of_nat x = UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2); x < 4096\<rbrakk> \<Longrightarrow> transform_pde pde = transform_pde (x3 (UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2))) proof (prove)
goal:
No subgoals!