theory ArchUntyped_AI

lemma store_pde_nonempty_table:
  "\<lbrace>\<lambda>s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r 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. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r 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 nonempty_table_def a_type_def) apply (clarsimp simp add: empty_table_def second_level_tables_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r 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 s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r 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 s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r 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> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state (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>))))) r (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>empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); \<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; r = pde_ptr && ~~ mask pd_bits; kheap s (pde_ptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (pde_ptr && mask pd_bits >> 2) then pde else pd a))) proof (prove)
goal:
No subgoals!