theory ArchUntyped_AI

lemma store_pde_global_global_objs:
  "\<lbrace>\<lambda>s. valid_global_objs s
           \<and> (\<forall>rf. pde_ref pde = Some rf \<longrightarrow>
                   rf \<in> set (arm_global_pts (arch_state s)))
           \<and> ucast (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots
           \<and> valid_pde_mappings pde\<rbrace>
   store_pde pde_ptr pde
   \<lbrace>\<lambda>rv s. valid_global_objs s\<rbrace>" apply (simp add: store_pde_def set_pd_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: obj_at_def fun_upd_def[symmetric]) proof - fix s pd assume vg: "valid_global_objs s"
     and gr: "\<forall>rf. pde_ref pde = Some rf \<longrightarrow>
                   rf \<in> set (arm_global_pts (arch_state s))"
     and uc: "ucast (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots"
     and vp: "valid_pde_mappings pde"
     and pd: "kheap s (pde_ptr && ~~ mask pd_bits) =
              Some (ArchObj (PageDirectory pd))" let ?ko' = "ArchObj (PageDirectory
                         (pd(ucast (pde_ptr && mask pd_bits >> 2) := pde)))" let ?s' = "s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ?ko')\<rparr>" have typ_at: "\<And>T p. typ_at T p s \<Longrightarrow> typ_at T p ?s'" using pd by (clarsimp simp: obj_at_def a_type_def) have valid_pde: "\<And>pde. valid_pde pde s \<Longrightarrow> valid_pde pde ?s'" by (case_tac pdea, auto simp add: typ_at data_at_def) have valid_pte: "\<And>pte. valid_pte pte s \<Longrightarrow> valid_pte pte ?s'" by (case_tac pte, auto simp add: typ_at data_at_def) have valid_ao_at: "\<And>p. valid_ao_at p s \<Longrightarrow> valid_ao_at p ?s'" using pd uc apply (clarsimp simp: valid_ao_at_def obj_at_def) apply (intro conjI impI allI) apply (clarsimp simp: valid_pde vp) apply (case_tac ao, simp_all add: typ_at valid_pde valid_pte) done have valid_vso_at: "\<And>p. valid_vso_at p s \<Longrightarrow> valid_vso_at p ?s'" using pd uc apply (clarsimp simp: valid_vso_at_def obj_at_def) apply (intro conjI impI allI) apply (clarsimp simp: valid_pde vp) apply (case_tac ao, simp_all add: typ_at valid_pde valid_pte) done have empty:
    "\<And>p. obj_at (empty_table (set (second_level_tables (arch_state s)))) p s
          \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) p ?s'" using pd gr vp uc by (clarsimp simp: obj_at_def empty_table_def second_level_tables_def) show "valid_global_objs ?s'" using vg pd apply (clarsimp simp add: valid_global_objs_def valid_ao_at valid_vso_at empty) apply (fastforce simp add: obj_at_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_global_objs s \<and> (\<forall>rf. pde_ref pde = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s))) \<and> UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots \<and> valid_pde_mappings pde\<rbrace> store_pde pde_ptr pde \<lbrace>\<lambda>rv. valid_global_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_global_objs s \<and> (\<forall>rf. pde_ref pde = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s))) \<and> UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots \<and> valid_pde_mappings pde\<rbrace> do pd <- get_pd (pde_ptr && ~~ mask pd_bits);
kobj <- get_object (pde_ptr && ~~ mask pd_bits);
y <- assert (a_type kobj = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>)
od \<lbrace>\<lambda>rv. valid_global_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_global_objs s \<and> (\<forall>rf. pde_ref pde = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s))) \<and> UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots \<and> valid_pde_mappings pde \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (pde_ptr && ~~ mask pd_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (pde_ptr && ~~ mask pd_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde)))) \<longrightarrow> valid_global_objs (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_global_objs s; \<forall>rf. pde_ref pde = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_pde_mappings pde; kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rbrakk> \<Longrightarrow> valid_global_objs (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (state)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_global_objs s; \<forall>rf. pde_ref pde = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_pde_mappings pde; kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rbrakk> \<Longrightarrow> valid_global_objs (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (state)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_global_objs s; \<forall>rf. pde_ref pde = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_pde_mappings pde; kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rbrakk> \<Longrightarrow> valid_global_objs (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (state)
this:
valid_global_objs s
\<forall>rf. pde_ref pde = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s))
UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots
valid_pde_mappings pde
kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))

goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_global_objs s; \<forall>rf. pde_ref pde = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_pde_mappings pde; kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rbrakk> \<Longrightarrow> valid_global_objs (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (state)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_global_objs s; \<forall>rf. pde_ref pde = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_pde_mappings pde; kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rbrakk> \<Longrightarrow> valid_global_objs (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (state)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_global_objs s; \<forall>rf. pde_ref pde = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_pde_mappings pde; kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rbrakk> \<Longrightarrow> valid_global_objs (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>T p. typ_at T p s \<Longrightarrow> typ_at T p (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
using this:
kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))

goal (1 subgoal):
 1. \<And>T p. typ_at T p s \<Longrightarrow> typ_at T p (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (state)
this:
typ_at ?T ?p s \<Longrightarrow> typ_at ?T ?p (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>)

goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_global_objs s; \<forall>rf. pde_ref pde = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_pde_mappings pde; kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rbrakk> \<Longrightarrow> valid_global_objs (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>pdea. valid_pde pdea s \<Longrightarrow> valid_pde pdea (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (state)
this:
valid_pde ?pde s \<Longrightarrow> valid_pde ?pde (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>)

goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_global_objs s; \<forall>rf. pde_ref pde = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_pde_mappings pde; kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rbrakk> \<Longrightarrow> valid_global_objs (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>pte. valid_pte pte s \<Longrightarrow> valid_pte pte (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (state)
this:
valid_pte ?pte s \<Longrightarrow> valid_pte ?pte (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>)

goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_global_objs s; \<forall>rf. pde_ref pde = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_pde_mappings pde; kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rbrakk> \<Longrightarrow> valid_global_objs (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>p. valid_ao_at p s \<Longrightarrow> valid_ao_at p (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
using this:
kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))
UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots

goal (1 subgoal):
 1. \<And>p. valid_ao_at p s \<Longrightarrow> valid_ao_at p (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s p = Some (ArchObj ao); valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> (p = pde_ptr && ~~ mask pd_bits \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<longrightarrow> valid_pde pde (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>)) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>)))) \<and> (p \<noteq> pde_ptr && ~~ mask pd_bits \<longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>p ao. \<lbrakk>kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s p = Some (ArchObj ao); valid_vspace_obj ao s; p = pde_ptr && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> \<forall>x\<in>- kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<longrightarrow> valid_pde pde (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>)) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>))
 2. \<And>p ao. \<lbrakk>kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s p = Some (ArchObj ao); valid_vspace_obj ao s; p \<noteq> pde_ptr && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s p = Some (ArchObj ao); valid_vspace_obj ao s; p \<noteq> pde_ptr && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal:
No subgoals! proof (state)
this:
valid_ao_at ?p s \<Longrightarrow> valid_ao_at ?p (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>)

goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_global_objs s; \<forall>rf. pde_ref pde = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_pde_mappings pde; kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rbrakk> \<Longrightarrow> valid_global_objs (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>p. valid_vso_at p s \<Longrightarrow> valid_vso_at p (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
using this:
kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))
UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots

goal (1 subgoal):
 1. \<And>p. valid_vso_at p s \<Longrightarrow> valid_vso_at p (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s p = Some (ArchObj ao); valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> (p = pde_ptr && ~~ mask pd_bits \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<longrightarrow> valid_pde pde (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>)) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>)))) \<and> (p \<noteq> pde_ptr && ~~ mask pd_bits \<longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>p ao. \<lbrakk>kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s p = Some (ArchObj ao); valid_vspace_obj ao s; p = pde_ptr && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> \<forall>x\<in>- kernel_mapping_slots. (x = UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<longrightarrow> valid_pde pde (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>)) \<and> (x \<noteq> UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<longrightarrow> valid_pde (pd x) (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>))
 2. \<And>p ao. \<lbrakk>kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s p = Some (ArchObj ao); valid_vspace_obj ao s; p \<noteq> pde_ptr && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; kheap s p = Some (ArchObj ao); valid_vspace_obj ao s; p \<noteq> pde_ptr && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal:
No subgoals! proof (state)
this:
valid_vso_at ?p s \<Longrightarrow> valid_vso_at ?p (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>)

goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_global_objs s; \<forall>rf. pde_ref pde = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_pde_mappings pde; kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rbrakk> \<Longrightarrow> valid_global_objs (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>p. obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) p (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
using this:
kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))
\<forall>rf. pde_ref pde = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s))
valid_pde_mappings pde
UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots

goal (1 subgoal):
 1. \<And>p. obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) p (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (state)
this:
obj_at (empty_table (set (second_level_tables (arch_state s)))) ?p s \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) ?p (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>)

goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>valid_global_objs s; \<forall>rf. pde_ref pde = Some rf \<longrightarrow> rf \<in> set (arm_global_pts (arch_state s)); UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_pde_mappings pde; kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); a_type (ArchObj (PageDirectory pd)) = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rbrakk> \<Longrightarrow> valid_global_objs (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. valid_global_objs (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
using this:
valid_global_objs s
kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))

goal (1 subgoal):
 1. valid_global_objs (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); p \<in> set (arm_global_pts (arch_state s)); valid_vso_at (arm_global_pd (arch_state s)) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) (arm_global_pd (arch_state s)) s; \<forall>p\<in>set (arm_global_pts (arch_state s)). \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> \<exists>pt. ako_at (PageTable pt) p (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>) \<and> (\<forall>x. aligned_pte (pt x)) proof (prove)
goal:
No subgoals! proof (state)
this:
valid_global_objs (s\<lparr>kheap := (kheap s)(pde_ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) := pde))))\<rparr>)

goal:
No subgoals!