theory ArchAcc_AI

lemma store_pte_valid_objs [wp]:
  "\<lbrace>(%s. wellformed_pte pte) and valid_objs\<rbrace> store_pte p pte \<lbrace>\<lambda>_. valid_objs\<rbrace>" apply (simp add: store_pte_def set_pt_def get_pt_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 pt_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_pte pte) and valid_objs\<rbrace> store_pte p pte \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. wellformed_pte pte) and valid_objs\<rbrace> do x <- gets kheap;
xa <- assert (\<exists>y. x (p && ~~ mask pt_bits) = Some y);
pt <- case the (x (p && ~~ mask pt_bits)) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
x <- gets kheap;
y <- assert (\<exists>y. x (p && ~~ mask pt_bits) = Some y);
y <- assert (a_type (the (x (p && ~~ mask pt_bits))) = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))\<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 pt_bits) = Some y);
pt <- case the (x (p && ~~ mask pt_bits)) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
x <- gets kheap;
y <- assert (\<exists>y. x (p && ~~ mask pt_bits) = Some y);
y <- assert (a_type (the (x (p && ~~ mask pt_bits))) = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))\<rparr>)
od \<lbrace>\<lambda>_. valid_objs\<rbrace>
 2. \<And>s. ((\<lambda>s. wellformed_pte pte) and valid_objs) s \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. wellformed_pte pte) and valid_objs) s \<Longrightarrow> (\<exists>y. kheap s (p && ~~ mask pt_bits) = Some y) \<longrightarrow> (\<forall>x xa. the (kheap s (p && ~~ mask pt_bits)) = CNode x xa \<longrightarrow> True) \<and> (\<forall>x. the (kheap s (p && ~~ mask pt_bits)) = TCB x \<longrightarrow> True) \<and> (\<forall>x. the (kheap s (p && ~~ mask pt_bits)) = Endpoint x \<longrightarrow> True) \<and> (\<forall>x. the (kheap s (p && ~~ mask pt_bits)) = Notification x \<longrightarrow> True) \<and> (\<forall>x. the (kheap s (p && ~~ mask pt_bits)) = ArchObj x \<longrightarrow> (\<forall>xa. x = ASIDPool xa \<longrightarrow> True) \<and> (\<forall>xa. x = PageTable xa \<longrightarrow> (\<exists>y. kheap s (p && ~~ mask pt_bits) = Some y) \<longrightarrow> a_type (the (kheap s (p && ~~ mask pt_bits))) = a_type (ArchObj (PageTable (xa(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) \<longrightarrow> valid_objs (s\<lparr>kheap := (kheap s)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))\<rparr>)) \<and> (\<forall>xa. x = PageDirectory xa \<longrightarrow> True) \<and> (\<forall>xa xb. x = DataPage xa xb \<longrightarrow> True)) proof (prove)
goal (1 subgoal):
 1. \<And>s xa ptr ya. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa)); a_type (ArchObj (PageTable xa)) = a_type (ArchObj (PageTable (xa(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya\<rbrakk> \<Longrightarrow> valid_obj ptr ya (s\<lparr>kheap := (kheap s)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> valid_obj ptr ya_ (s_\<lparr>kheap := (kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> valid_obj ptr ya_ s_
 2. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> valid_obj (p && ~~ mask pt_bits) (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) s_
 3. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> kheap s_ (p && ~~ mask pt_bits) = Some ?ko
 4. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) = a_type ?ko proof (prove)
goal (5 subgoals):
 1. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_; ptr = p && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> valid_obj ptr ya_ s_
 2. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_; ptr \<noteq> p && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> valid_obj ptr ya_ s_
 3. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> valid_obj (p && ~~ mask pt_bits) (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) s_
 4. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> kheap s_ (p && ~~ mask pt_bits) = Some ?ko
 5. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) = a_type ?ko proof (prove)
goal (5 subgoals):
 1. \<lbrakk>wellformed_pte pte; kheap s_ (p && ~~ mask pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_; ptr = p && ~~ mask pt_bits; \<exists>obj. kheap s_ (p && ~~ mask pt_bits) = Some obj \<and> valid_obj (p && ~~ mask pt_bits) obj s_\<rbrakk> \<Longrightarrow> valid_obj ptr ya_ s_
 2. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_; ptr \<noteq> p && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> valid_obj ptr ya_ s_
 3. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> valid_obj (p && ~~ mask pt_bits) (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) s_
 4. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> kheap s_ (p && ~~ mask pt_bits) = Some ?ko
 5. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) = a_type ?ko proof (prove)
goal (4 subgoals):
 1. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_; ptr \<noteq> p && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> valid_obj ptr ya_ s_
 2. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> valid_obj (p && ~~ mask pt_bits) (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) s_
 3. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> kheap s_ (p && ~~ mask pt_bits) = Some ?ko
 4. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) = a_type ?ko proof (prove)
goal (4 subgoals):
 1. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); kheap s_ ptr = Some ya_; ptr \<noteq> p && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> valid_obj ptr ya_ s_
 2. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> valid_obj (p && ~~ mask pt_bits) (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) s_
 3. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> kheap s_ (p && ~~ mask pt_bits) = Some ?ko
 4. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) = a_type ?ko proof (prove)
goal (3 subgoals):
 1. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> valid_obj (p && ~~ mask pt_bits) (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) s_
 2. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> kheap s_ (p && ~~ mask pt_bits) = Some ?ko
 3. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) = a_type ?ko proof (prove)
goal (3 subgoals):
 1. \<lbrakk>wellformed_pte pte; kheap s_ (p && ~~ mask pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_; \<exists>obj. kheap s_ (p && ~~ mask pt_bits) = Some obj \<and> valid_obj (p && ~~ mask pt_bits) obj s_\<rbrakk> \<Longrightarrow> valid_obj (p && ~~ mask pt_bits) (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) s_
 2. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> kheap s_ (p && ~~ mask pt_bits) = Some ?ko
 3. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) = a_type ?ko proof (prove)
goal (2 subgoals):
 1. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> kheap s_ (p && ~~ mask pt_bits) = Some ?ko
 2. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) = a_type ?ko proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wellformed_pte pte; \<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 pt_bits) = Some (ArchObj (PageTable xa_)); a_type (ArchObj (PageTable xa_)) = a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))); ((kheap s_)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))) ptr = Some ya_\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageTable (xa_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) = a_type (ArchObj (PageTable xa_)) proof (prove)
goal:
No subgoals!