theory ArchRetype_AI

lemma store_pde_global_objs[wp]:
  "\<lbrace>valid_global_objs and valid_global_refs and
    valid_arch_state and
    (\<lambda>s. (\<forall>pd. (obj_at (empty_table (set (second_level_tables (arch_state s))))
                   (p && ~~ mask pd_bits) s
           \<and> ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s
             \<longrightarrow> empty_table (set (second_level_tables (arch_state s)))
                                 (ArchObj (PageDirectory (pd(ucast (p && mask pd_bits >> 2) := pde))))))
        \<or> (\<exists>slot. cte_wp_at (\<lambda>cap. p && ~~ mask pd_bits \<in> obj_refs cap) slot s))\<rbrace>
     store_pde p pde \<lbrace>\<lambda>rv. valid_global_objs\<rbrace>" apply (simp add: store_pde_def) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_objs and valid_global_refs and valid_arch_state and (\<lambda>s. (\<forall>pd. obj_at (empty_table (set (second_level_tables (arch_state s)))) (p && ~~ mask pd_bits) s \<and> ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) \<or> (\<exists>slot. cte_wp_at (\<lambda>cap. p && ~~ mask pd_bits \<in> obj_refs cap) slot s))\<rbrace> store_pde p pde \<lbrace>\<lambda>rv. valid_global_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_objs and valid_global_refs and valid_arch_state and (\<lambda>s. (\<forall>pd. obj_at (empty_table (set (second_level_tables (arch_state s)))) (p && ~~ mask pd_bits) s \<and> ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. p && ~~ mask pd_bits \<in> obj_refs cap) (a, b) s))\<rbrace> do pd <- get_pd (p && ~~ mask pd_bits);
set_pd (p && ~~ mask pd_bits) (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))
od \<lbrace>\<lambda>rv. valid_global_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_global_objs and valid_global_refs and valid_arch_state and (\<lambda>s. (\<forall>pd. obj_at (empty_table (set (second_level_tables (arch_state s)))) (p && ~~ mask pd_bits) s \<and> ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. p && ~~ mask pd_bits \<in> obj_refs cap) (a, b) s))) s \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (valid_global_objs and valid_global_refs and valid_arch_state and (\<lambda>s. (obj_at (empty_table (set (second_level_tables (arch_state s)))) (p && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))) \<or> (\<exists>slot. cte_wp_at (\<lambda>cap. p && ~~ mask pd_bits \<in> obj_refs cap) slot s))) s proof (prove)
goal:
No subgoals!