theory Finalise_DR

lemma dcorres_store_pte_non_sense:
  "dcorres dc \<top> (valid_idle and
     (\<lambda>s. \<exists>f. ko_at (ArchObj (arch_kernel_obj.PageTable f)) (slot && ~~ mask pt_bits) s
      \<and> (f (ucast (slot && mask pt_bits >> 2)) = pte)))
  (return a) (store_pte slot pte)" apply (simp add:store_pte_def) apply (simp add:get_pt_def bind_assoc set_object_def get_object_def set_pt_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_table_at_rev) apply (drule(1) page_table_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.PageTable f) (slot && ~~ mask pt_bits) s \<and> f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = pte)) (return a) (store_pte slot pte) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageTable f) (slot && ~~ mask pt_bits) s \<and> f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = pte)) (return a) (do pt <- get_pt (slot && ~~ mask pt_bits);
set_pt (slot && ~~ mask pt_bits) (pt(UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2) := pte))
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageTable f) (slot && ~~ mask pt_bits) s \<and> f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = pte)) (return a) (do x <- get;
xa <- assert (\<exists>y. kheap x (slot && ~~ mask pt_bits) = Some y);
pt <- case the (kheap x (slot && ~~ mask pt_bits)) of ArchObj (arch_kernel_obj.PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
x <- get;
y <- assert (\<exists>y. kheap x (slot && ~~ mask pt_bits) = Some y);
y <- assert (a_type (the (kheap x (slot && ~~ mask pt_bits))) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2) := pte)))));
s <- get;
put (update_kheap ((kheap s)(slot && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2) := pte))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; (valid_idle and (\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageTable f) (slot && ~~ mask pt_bits) s \<and> f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)) = pte)) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return a) (do x <- assert (\<exists>y. kheap s' (slot && ~~ mask pt_bits) = Some y);
pt <- case the (kheap s' (slot && ~~ mask pt_bits)) of ArchObj (arch_kernel_obj.PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
x <- get;
y <- assert (\<exists>y. kheap x (slot && ~~ mask pt_bits) = Some y);
y <- assert (a_type (the (kheap x (slot && ~~ mask pt_bits))) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2) := pte)))));
s <- get;
put (update_kheap ((kheap s)(slot && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2) := pte))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' x2 f. \<lbrakk>valid_idle s'; ako_at (arch_kernel_obj.PageTable f) (slot && ~~ mask pt_bits) s'; pte = f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)); kheap s' (slot && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return a) (do x <- get;
y <- if \<exists>y. kheap x (slot && ~~ mask pt_bits) = Some y then return () else fail;
y <- if a_type (the (kheap x (slot && ~~ mask pt_bits))) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2) := f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)))))) then return () else fail;
s <- get;
put (update_kheap ((kheap s)(slot && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2) := f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2))))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' x2 f s'a. \<lbrakk>valid_idle s'; ako_at (arch_kernel_obj.PageTable f) (slot && ~~ mask pt_bits) s'; pte = f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)); kheap s' (slot && ~~ 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) (return a) (do y <- if \<exists>y. kheap s'a (slot && ~~ mask pt_bits) = Some y then return () else fail;
y <- if a_type (the (kheap s'a (slot && ~~ mask pt_bits))) = a_type (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2) := f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)))))) then return () else fail;
s <- get;
put (update_kheap ((kheap s)(slot && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2) := f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2))))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x2 f s'a. \<lbrakk>valid_idle s'a; ako_at (arch_kernel_obj.PageTable f) (slot && ~~ mask pt_bits) s'a; pte = f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)); kheap s'a (slot && ~~ 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) (slot && mask pt_bits >> 2) := f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2))))))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (return a) (do s <- get;
put (update_kheap ((kheap s)(slot && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2) := f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2))))))) s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x2 f s'a. \<lbrakk>valid_idle s'a; ako_at (arch_kernel_obj.PageTable f) (slot && ~~ mask pt_bits) s'a; pte = f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)); kheap s'a (slot && ~~ 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) (slot && mask pt_bits >> 2) := f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2))))))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (return a) (do s <- get;
\<lambda>_. ({((), update_kheap ((kheap s)(slot && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2) := f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2))))))) s)}, False)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x2 f s'a s'. \<lbrakk>valid_idle s'a; ako_at (arch_kernel_obj.PageTable f) (slot && ~~ mask pt_bits) s'a; pte = f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)); kheap s'a (slot && ~~ 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) (slot && mask pt_bits >> 2) := f (UCAST(32 \<rightarrow> 8) (slot && mask pt_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 pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2) := f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2))))))) s')}, False)) proof (prove)
goal (1 subgoal):
 1. \<And>x2 f s'a s'. \<lbrakk>valid_idle s'; ako_at (arch_kernel_obj.PageTable f) (slot && ~~ mask pt_bits) s'; pte = f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)); kheap s' (slot && ~~ 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) (slot && mask pt_bits >> 2) := f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)))))); s'a = s'\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(slot && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2) := f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2))))))) s') = transform_objects s' proof (prove)
goal (1 subgoal):
 1. \<And>x2 f s'a s'. \<lbrakk>valid_idle s'; ako_at (arch_kernel_obj.PageTable f) (slot && ~~ mask pt_bits) s'; pte = f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)); kheap s' (slot && ~~ 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) (slot && mask pt_bits >> 2) := f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)))))); s'a = s'; typ_at (AArch APageTable) (slot && ~~ mask pt_bits) s'\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(slot && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2) := f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2))))))) s') = transform_objects s' proof (prove)
goal (1 subgoal):
 1. \<And>x2 f s'a s'. \<lbrakk>valid_idle s'; ako_at (arch_kernel_obj.PageTable f) (slot && ~~ mask pt_bits) s'; pte = f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)); kheap s' (slot && ~~ 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) (slot && mask pt_bits >> 2) := f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)))))); s'a = s'; not_idle_thread (slot && ~~ mask pt_bits) s'\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(slot && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2) := f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2))))))) s') = transform_objects s' proof (prove)
goal (1 subgoal):
 1. \<And>x2 f s'a s' x. \<lbrakk>valid_idle s'; ako_at (arch_kernel_obj.PageTable f) (slot && ~~ mask pt_bits) s'; pte = f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)); kheap s' (slot && ~~ 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) (slot && mask pt_bits >> 2) := f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2)))))); s'a = s'; not_idle_thread (slot && ~~ mask pt_bits) s'\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s')(slot && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2) := f (UCAST(32 \<rightarrow> 8) (slot && mask pt_bits >> 2))))))) s') x = transform_objects s' x proof (prove)
goal:
No subgoals!