theory ArchAcc_AI

lemma store_pde_valid_objs [wp]:
  "\<lbrace>(%s. wellformed_pde pde) and valid_objs\<rbrace> store_pde p pde \<lbrace>\<lambda>_. valid_objs\<rbrace>" apply (simp add: store_pde_def set_pd_def get_pd_def bind_assoc set_object_def get_object_def) apply (rule hoare_pre) apply (wp|wpc)+ apply (clarsimp simp: valid_objs_def dom_def simp del: fun_upd_apply) subgoal for \<dots> ptr _ apply (rule valid_obj_same_type) apply (cases "ptr = p && ~~ mask pd_bits") apply (erule allE, erule impE, blast) apply (clarsimp simp: valid_obj_def arch_valid_obj_def) apply clarsimp apply fastforce apply (erule allE, erule impE, blast) apply (clarsimp simp: valid_obj_def arch_valid_obj_def) apply assumption by (simp add: a_type_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. wellformed_pde pde) and valid_objs\<rbrace> store_pde p pde \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. wellformed_pde pde) and valid_objs\<rbrace> do x <- gets kheap;
xa <- assert (\<exists>y. x (p && ~~ mask pd_bits) = Some y);
pd <- case the (x (p && ~~ mask pd_bits)) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
x <- gets kheap;
y <- assert (\<exists>y. x (p && ~~ mask pd_bits) = Some y);
y <- assert (a_type (the (x (p && ~~ mask pd_bits))) = 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>_. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> do x <- gets kheap;
xa <- assert (\<exists>y. x (p && ~~ mask pd_bits) = Some y);
pd <- case the (x (p && ~~ mask pd_bits)) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
x <- gets kheap;
y <- assert (\<exists>y. x (p && ~~ mask pd_bits) = Some y);
y <- assert (a_type (the (x (p && ~~ mask pd_bits))) = 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>_. valid_objs\<rbrace>
 2. \<And>s. ((\<lambda>s. wellformed_pde pde) and valid_objs) s \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. wellformed_pde pde) and valid_objs) s \<Longrightarrow> (\<exists>y. kheap s (p && ~~ mask pd_bits) = Some y) \<longrightarrow> (\<forall>x xa. the (kheap s (p && ~~ mask pd_bits)) = CNode x xa \<longrightarrow> True) \<and> (\<forall>x. the (kheap s (p && ~~ mask pd_bits)) = TCB x \<longrightarrow> True) \<and> (\<forall>x. the (kheap s (p && ~~ mask pd_bits)) = Endpoint x \<longrightarrow> True) \<and> (\<forall>x. the (kheap s (p && ~~ mask pd_bits)) = Notification x \<longrightarrow> True) \<and> (\<forall>x. the (kheap s (p && ~~ mask pd_bits)) = ArchObj x \<longrightarrow> (\<forall>xa. x = ASIDPool xa \<longrightarrow> True) \<and> (\<forall>xa. x = PageTable xa \<longrightarrow> True) \<and> (\<forall>xa. x = PageDirectory xa \<longrightarrow> (\<exists>y. kheap s (p && ~~ mask pd_bits) = Some y) \<longrightarrow> a_type (the (kheap s (p && ~~ mask pd_bits))) = a_type (ArchObj (PageDirectory (xa(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) \<longrightarrow> valid_objs (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rparr>)) \<and> (\<forall>xa xb. x = DataPage xa xb \<longrightarrow> True)) proof (prove)
goal (1 subgoal):
 1. \<And>s xa ptr ya. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa)); a_type (ArchObj (PageDirectory xa)) = a_type (ArchObj (PageDirectory (xa(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya\<rbrakk> \<Longrightarrow> valid_obj ptr ya (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> valid_obj ptr ya_ (s_\<lparr>kheap := (kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> valid_obj ptr ya_ s_
 2. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> valid_obj (p && ~~ mask pd_bits) (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) s_
 3. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> kheap s_ (p && ~~ mask pd_bits) = Some ?ko
 4. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = a_type ?ko proof (prove)
goal (5 subgoals):
 1. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_; ptr = p && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> valid_obj ptr ya_ s_
 2. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_; ptr \<noteq> p && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> valid_obj ptr ya_ s_
 3. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> valid_obj (p && ~~ mask pd_bits) (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) s_
 4. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> kheap s_ (p && ~~ mask pd_bits) = Some ?ko
 5. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = a_type ?ko proof (prove)
goal (5 subgoals):
 1. \<lbrakk>wellformed_pde pde; kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_; ptr = p && ~~ mask pd_bits; \<exists>obj. kheap s_ (p && ~~ mask pd_bits) = Some obj \<and> valid_obj (p && ~~ mask pd_bits) obj s_\<rbrakk> \<Longrightarrow> valid_obj ptr ya_ s_
 2. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_; ptr \<noteq> p && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> valid_obj ptr ya_ s_
 3. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> valid_obj (p && ~~ mask pd_bits) (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) s_
 4. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> kheap s_ (p && ~~ mask pd_bits) = Some ?ko
 5. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = a_type ?ko proof (prove)
goal (4 subgoals):
 1. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_; ptr \<noteq> p && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> valid_obj ptr ya_ s_
 2. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> valid_obj (p && ~~ mask pd_bits) (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) s_
 3. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> kheap s_ (p && ~~ mask pd_bits) = Some ?ko
 4. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = a_type ?ko proof (prove)
goal (4 subgoals):
 1. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); kheap s_ ptr = Some ya_; ptr \<noteq> p && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> valid_obj ptr ya_ s_
 2. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> valid_obj (p && ~~ mask pd_bits) (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) s_
 3. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> kheap s_ (p && ~~ mask pd_bits) = Some ?ko
 4. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = a_type ?ko proof (prove)
goal (3 subgoals):
 1. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> valid_obj (p && ~~ mask pd_bits) (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) s_
 2. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> kheap s_ (p && ~~ mask pd_bits) = Some ?ko
 3. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = a_type ?ko proof (prove)
goal (3 subgoals):
 1. \<lbrakk>wellformed_pde pde; kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_; \<exists>obj. kheap s_ (p && ~~ mask pd_bits) = Some obj \<and> valid_obj (p && ~~ mask pd_bits) obj s_\<rbrakk> \<Longrightarrow> valid_obj (p && ~~ mask pd_bits) (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) s_
 2. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> kheap s_ (p && ~~ mask pd_bits) = Some ?ko
 3. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = a_type ?ko proof (prove)
goal (2 subgoals):
 1. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> kheap s_ (p && ~~ mask pd_bits) = Some ?ko
 2. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = a_type ?ko proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wellformed_pde pde; \<forall>ptr. (\<exists>y. kheap s_ ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s_ ptr = Some obj \<and> valid_obj ptr obj s_); kheap s_ (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory xa_)); a_type (ArchObj (PageDirectory xa_)) = a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))); ((kheap s_)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageDirectory (xa_(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) = a_type (ArchObj (PageDirectory xa_)) proof (prove)
goal:
No subgoals!