theory ArchCNode_AC

lemma store_pde_st_vrefs[wp]:
  "\<lbrace>\<lambda>s. \<forall>S. P ((state_vrefs s) (p && ~~ mask pd_bits :=
                                  (state_vrefs s (p && ~~ mask pd_bits) - S) \<union>
                                  (if ucast (kernel_base >> 20) \<le> (ucast (p && mask pd_bits >> 2)::12 word)
                                   then {}
                                   else (\<Union>(p', sz, auth)\<in>set_option (pde_ref2 pde).
                                        (\<lambda>(p'', a). (p'', (p && mask pd_bits) >> 2, APageDirectory, a)) `
                                                                             (ptr_range p' sz \<times> auth)))))\<rbrace>
   store_pde p pde
   \<lbrace>\<lambda>rv s. P (state_vrefs s)\<rbrace>" apply (simp add: store_pde_def set_pd_def set_object_def split del: if_split) apply (wp get_object_wp) apply (clarsimp simp: obj_at_def) apply (erule all_rsubst[where P=P], subst fun_eq_iff) apply (clarsimp simp add: state_vrefs_def vs_refs_no_global_pts_def
                            fun_upd_def[symmetric] fun_upd_comp) apply (cases "pde_ref2 pde") by (auto simp: split_def insert_Diff_if Un_ac ucast_ucast_mask_shift_helper)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>S. P ((state_vrefs s)(p && ~~ mask pd_bits := state_vrefs s (p && ~~ mask pd_bits) - S \<union> (if UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then {} else \<Union>(p', sz, auth)\<in>set_option (pde_ref2 pde). (\<lambda>(p'', a). (p'', p && mask pd_bits >> 2, APageDirectory, a)) ` (ptr_range p' sz \<times> auth))))\<rbrace> store_pde p pde \<lbrace>\<lambda>rv s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>S. P ((state_vrefs s)(p && ~~ mask pd_bits := state_vrefs s (p && ~~ mask pd_bits) - S \<union> (if UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then {} else \<Union>x\<in>set_option (pde_ref2 pde). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pd_bits >> 2, APageDirectory, a)) ` (ptr_range p' sz \<times> auth))))\<rbrace> do pd <- get_pd (p && ~~ mask pd_bits);
kobj <- get_object (p && ~~ mask pd_bits);
y <- assert (a_type kobj = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rparr>)
od \<lbrace>\<lambda>rv s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>S. P ((state_vrefs s)(p && ~~ mask pd_bits := state_vrefs s (p && ~~ mask pd_bits) - S \<union> (if UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then {} else \<Union>x\<in>set_option (pde_ref2 pde). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pd_bits >> 2, APageDirectory, a)) ` (ptr_range p' sz \<times> auth)))) \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (p && ~~ mask pd_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) \<longrightarrow> P (state_vrefs (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>\<forall>S. P ((state_vrefs s)(p && ~~ mask pd_bits := state_vrefs s (p && ~~ mask pd_bits) - S \<union> (if UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then {} else \<Union>x\<in>set_option (pde_ref2 pde). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pd_bits >> 2, APageDirectory, a)) ` (ptr_range p' sz \<times> auth)))); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rbrakk> \<Longrightarrow> P (state_vrefs (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pd a))) else kheap s a\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rbrakk> \<Longrightarrow> \<exists>S. \<forall>x. ((state_vrefs s)(p && ~~ mask pd_bits := state_vrefs s (p && ~~ mask pd_bits) - S \<union> (if UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then {} else \<Union>(p', sz, auth)\<in>set_option (pde_ref2 pde). (\<lambda>(p'', a). (p'', p && mask pd_bits >> 2, APageDirectory, a)) ` (ptr_range p' sz \<times> auth)))) x = state_vrefs (s\<lparr>kheap := \<lambda>a. if a = p && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) then pde else pd a))) else kheap s a\<rparr>) x proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<exists>S. (\<Union>x\<in>graph_of (pde_ref2 \<circ> pd) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) - S = (\<Union>x\<in>graph_of ((pde_ref2 \<circ> pd)(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde_ref2 pde)) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)))) \<and> (\<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<exists>S. (\<Union>x\<in>graph_of (pde_ref2 \<circ> pd) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) - S \<union> (\<Union>x\<in>set_option (pde_ref2 pde). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pd_bits >> 2, APageDirectory, a)) ` (ptr_range p' sz \<times> auth)) = (\<Union>x\<in>graph_of ((pde_ref2 \<circ> pd)(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde_ref2 pde)) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)))) proof (prove)
goal (2 subgoals):
 1. \<And>s pd. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); pde_ref2 pde = None\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<exists>S. (\<Union>x\<in>graph_of (pde_ref2 \<circ> pd) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) - S = (\<Union>x\<in>graph_of ((pde_ref2 \<circ> pd)(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde_ref2 pde)) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)))) \<and> (\<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<exists>S. (\<Union>x\<in>graph_of (pde_ref2 \<circ> pd) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) - S \<union> (\<Union>x\<in>set_option (pde_ref2 pde). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pd_bits >> 2, APageDirectory, a)) ` (ptr_range p' sz \<times> auth)) = (\<Union>x\<in>graph_of ((pde_ref2 \<circ> pd)(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde_ref2 pde)) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth))))
 2. \<And>s pd a. \<lbrakk>kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); pde_ref2 pde = Some a\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<exists>S. (\<Union>x\<in>graph_of (pde_ref2 \<circ> pd) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) - S = (\<Union>x\<in>graph_of ((pde_ref2 \<circ> pd)(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde_ref2 pde)) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)))) \<and> (\<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<longrightarrow> (\<exists>S. (\<Union>x\<in>graph_of (pde_ref2 \<circ> pd) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth)) - S \<union> (\<Union>x\<in>set_option (pde_ref2 pde). case x of (p', sz, auth) \<Rightarrow> (\<lambda>x. case x of (p'', a) \<Rightarrow> (p'', p && mask pd_bits >> 2, APageDirectory, a)) ` (ptr_range p' sz \<times> auth)) = (\<Union>x\<in>graph_of ((pde_ref2 \<circ> pd)(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde_ref2 pde)) - {(x, y). UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> x}. case x of (r, p, sz, auth) \<Rightarrow> (\<lambda>x. case x of (p, a) \<Rightarrow> (p, UCAST(12 \<rightarrow> 32) r, APageDirectory, a)) ` (ptr_range p sz \<times> auth))))