theory Finalise_DR

lemma dcorres_store_pde_non_sense:
  "dcorres dc \<top> (valid_idle and
     (\<lambda>s. \<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (slot && ~~ mask pd_bits) s
     \<and> (f (ucast (slot && mask pd_bits >> 2)) = pde)))
  (return a) (store_pde slot pde)" apply (simp add:store_pde_def) apply (simp add:get_pd_def bind_assoc set_object_def get_object_def set_pd_def gets_def) apply (rule dcorres_absorb_get_r) apply (clarsimp simp add:assert_def corres_free_fail
                  split:Structures_A.kernel_object.splits arch_kernel_obj.splits) apply (rule dcorres_absorb_get_r) apply (clarsimp simp:corres_free_fail
                  split:Structures_A.kernel_object.splits arch_kernel_obj.splits) apply (simp add:set_object_def put_def) apply (rule dcorres_absorb_get_r) apply (simp add:corres_underlying_def return_def transform_def transform_current_thread_def) apply (frule page_directory_at_rev) apply (drule(1) page_directory_not_idle[rotated]) apply (rule ext)+ apply (simp add:transform_objects_def not_idle_thread_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = pde)) (return a) (store_pde slot pde) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = pde)) (return a) (do pd <- get_pd (slot && ~~ mask pd_bits);
set_pd (slot && ~~ mask pd_bits) (pd(UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2) := pde))
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = pde)) (return a) (do x <- get;
xa <- assert (\<exists>y. kheap x (slot && ~~ mask pd_bits) = Some y);
pd <- case the (kheap x (slot && ~~ 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 (slot && ~~ mask pd_bits) = Some y);
y <- assert (a_type (the (kheap x (slot && ~~ mask pd_bits))) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pd(UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2) := pde)))));
s <- get;
put (update_kheap ((kheap s)(slot && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (pd(UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2) := pde))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)) = pde)) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return a) (do x <- assert (\<exists>y. kheap s' (slot && ~~ mask pd_bits) = Some y);
pd <- case the (kheap s' (slot && ~~ 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 (slot && ~~ mask pd_bits) = Some y);
y <- assert (a_type (the (kheap x (slot && ~~ mask pd_bits))) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pd(UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2) := pde)))));
s <- get;
put (update_kheap ((kheap s)(slot && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (pd(UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2) := pde))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3 f. \<lbrakk>valid_idle s'; ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s'; pde = f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)); kheap s' (slot && ~~ 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 (slot && ~~ mask pd_bits) = Some y then return () else fail;
y <- if a_type (the (kheap x (slot && ~~ mask pd_bits))) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2) := f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)))))) then return () else fail;
s <- get;
put (update_kheap ((kheap s)(slot && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2) := f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2))))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3 f s'a. \<lbrakk>valid_idle s'; ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s'; pde = f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)); kheap s' (slot && ~~ 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 (slot && ~~ mask pd_bits) = Some y then return () else fail;
y <- if a_type (the (kheap s'a (slot && ~~ mask pd_bits))) = a_type (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2) := f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)))))) then return () else fail;
s <- get;
put (update_kheap ((kheap s)(slot && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2) := f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2))))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x3 f s'a. \<lbrakk>valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s'a; pde = f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)); kheap s'a (slot && ~~ 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) (slot && mask pd_bits >> 2) := f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2))))))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (return a) (do s <- get;
put (update_kheap ((kheap s)(slot && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2) := f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2))))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x3 f s'a. \<lbrakk>valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s'a; pde = f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)); kheap s'a (slot && ~~ 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) (slot && mask pd_bits >> 2) := f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2))))))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (return a) (do s <- get;
\<lambda>_. ({((), update_kheap ((kheap s)(slot && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2) := f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2))))))) s)}, False)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x3 f s'a s'. \<lbrakk>valid_idle s'a; ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s'a; pde = f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)); kheap s'a (slot && ~~ 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) (slot && mask pd_bits >> 2) := f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)))))); transform s'a = transform s'; s'a = s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return a) (\<lambda>_. ({((), update_kheap ((kheap s')(slot && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2) := f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2))))))) s')}, False)) proof (prove)
goal (1 subgoal):
 1. \<And>x3 f s'a s'. \<lbrakk>valid_idle s'; ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s'; pde = f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)); kheap s' (slot && ~~ 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) (slot && mask pd_bits >> 2) := f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)))))); s'a = s'\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(slot && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2) := f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2))))))) s') = transform_objects s' proof (prove)
goal (1 subgoal):
 1. \<And>x3 f s'a s'. \<lbrakk>valid_idle s'; ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s'; pde = f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)); kheap s' (slot && ~~ 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) (slot && mask pd_bits >> 2) := f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)))))); s'a = s'; typ_at (AArch APageDirectory) (slot && ~~ mask pd_bits) s'\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(slot && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2) := f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2))))))) s') = transform_objects s' proof (prove)
goal (1 subgoal):
 1. \<And>x3 f s'a s'. \<lbrakk>valid_idle s'; ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s'; pde = f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)); kheap s' (slot && ~~ 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) (slot && mask pd_bits >> 2) := f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)))))); s'a = s'; not_idle_thread (slot && ~~ mask pd_bits) s'\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(slot && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2) := f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2))))))) s') = transform_objects s' proof (prove)
goal (1 subgoal):
 1. \<And>x3 f s'a s' x. \<lbrakk>valid_idle s'; ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s'; pde = f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)); kheap s' (slot && ~~ 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) (slot && mask pd_bits >> 2) := f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2)))))); s'a = s'; not_idle_thread (slot && ~~ mask pd_bits) s'\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(slot && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2) := f (UCAST(32 \<rightarrow> 12) (slot && mask pd_bits >> 2))))))) s') x = transform_objects s' x proof (prove)
goal:
No subgoals!