theory ArchCSpaceInvPre_AI

lemma set_cap_valid_arch_caps:
  "\<lbrace>\<lambda>s. valid_arch_caps s
      \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') ptr s
                \<longrightarrow> vs_cap_ref cap' = Some vref
                \<longrightarrow> (vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap')
                 \<or> (\<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s)
                 \<or> (\<forall>oref \<in> obj_refs cap'. \<not> (vref \<unrhd> oref) s))
      \<and> no_cap_to_obj_with_diff_ref cap {ptr} s
      \<and> ((is_pt_cap cap \<or> is_pd_cap cap) \<longrightarrow> cap_asid cap = None
            \<longrightarrow> (\<forall>r \<in> obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s))
      \<and> ((is_pt_cap cap \<or> is_pd_cap cap)
             \<longrightarrow> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow>
                  (is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap)
                    \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None)
                    \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap)
             \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap
                                              \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap')
                                              \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = ptr))\<rbrace>
     set_cap cap ptr
   \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>" apply (simp add: valid_arch_caps_def pred_conj_def) apply (wp set_cap_valid_vs_lookup set_cap_valid_table_caps
            set_cap_unique_table_caps set_cap_unique_table_refs) by simp_all blast+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_arch_caps s \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref cap {ptr} s \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = ptr))\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_vs_lookup s \<and> valid_table_caps s \<and> unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s) \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref cap {ptr} s \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pt_cap cap \<longrightarrow> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> (is_pt_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<and> (is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap)) \<longrightarrow> (\<forall>a b. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) (a, b) s \<longrightarrow> (a, b) = ptr)) \<and> (is_pd_cap cap \<longrightarrow> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> (is_pt_cap cap \<and> is_pt_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<and> (is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap)) \<longrightarrow> (\<forall>a b. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) (a, b) s \<longrightarrow> (a, b) = ptr))\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv x. valid_vs_lookup x \<and> valid_table_caps x \<and> unique_table_caps (caps_of_state x) \<and> unique_table_refs (caps_of_state x)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_vs_lookup s \<and> valid_table_caps s \<and> unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s) \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref cap {ptr} s \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pt_cap cap \<longrightarrow> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> (is_pt_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<and> (is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap)) \<longrightarrow> (\<forall>a b. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) (a, b) s \<longrightarrow> (a, b) = ptr)) \<and> (is_pd_cap cap \<longrightarrow> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> (is_pt_cap cap \<and> is_pt_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<and> (is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap)) \<longrightarrow> (\<forall>a b. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) (a, b) s \<longrightarrow> (a, b) = ptr)) \<Longrightarrow> (valid_vs_lookup s \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') ptr s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s)) \<and> unique_table_refs (caps_of_state s)) \<and> (valid_table_caps s \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s))) \<and> (unique_table_caps (caps_of_state s) \<and> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = ptr))) \<and> unique_table_refs (caps_of_state s) \<and> no_cap_to_obj_with_diff_ref cap {ptr} s