theory Finalise_DR

lemma store_pde_non_sense_wp:
  "\<lbrace>\<lambda>s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (slot && ~~ mask pd_bits) s
    \<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pd_bits >> 2)) = ARM_A.pde.InvalidPDE)) \<rbrace>
  store_pde x ARM_A.pde.InvalidPDE
   \<lbrace>\<lambda>r s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (slot && ~~ mask pd_bits) s
    \<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pd_bits >> 2)) = ARM_A.pde.InvalidPDE))\<rbrace>" apply (simp add:store_pde_def get_object_def get_pde_def set_pd_def set_object_def) apply wp apply (clarsimp simp:obj_at_def split:Structures_A.kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set xs. f (UCAST('b \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)\<rbrace> store_pde x InvalidPDE \<lbrace>\<lambda>r s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set xs. f (UCAST('b \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set xs. f (UCAST('b \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)\<rbrace> do pd <- get_pd (x && ~~ mask pd_bits);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh (x && ~~ mask pd_bits) = Some y);
return (the (kh (x && ~~ mask pd_bits)))
od;
y <- assert (a_type kobj = a_type (ArchObj (arch_kernel_obj.PageDirectory (pd(UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) := InvalidPDE)))));
s <- get;
put (update_kheap ((kheap s)(x && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (pd(UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) := InvalidPDE))))) s)
od \<lbrace>\<lambda>r s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set xs. f (UCAST('b \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) s \<and> (\<forall>slot\<in>set xs. f (UCAST('b \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE) \<Longrightarrow> \<forall>pd. ako_at (arch_kernel_obj.PageDirectory pd) (x && ~~ mask pd_bits) s \<longrightarrow> (\<exists>y. kheap s (x && ~~ mask pd_bits) = Some y) \<longrightarrow> a_type (the (kheap s (x && ~~ mask pd_bits))) = a_type (ArchObj (arch_kernel_obj.PageDirectory (pd(UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) := InvalidPDE)))) \<longrightarrow> (\<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (slot && ~~ mask pd_bits) (update_kheap ((kheap s)(x && ~~ mask pd_bits \<mapsto> ArchObj (arch_kernel_obj.PageDirectory (pd(UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) := InvalidPDE))))) s) \<and> (\<forall>slot\<in>set xs. f (UCAST('b \<rightarrow> 12) (slot && mask pd_bits >> 2)) = InvalidPDE)) proof (prove)
goal:
No subgoals!