theory ArchAcc_AI

lemma set_pt_arch_caps [wp]:
  "\<lbrace>valid_arch_caps and valid_arch_state and valid_vspace_objs and
    (\<lambda>s. valid_caps (caps_of_state s) s) and
    (\<lambda>s. ((\<exists>slot. caps_of_state s slot =
                 Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow>
          pt = (\<lambda>x. InvalidPTE)) \<or>
         (\<forall>slot. \<exists>asid. caps_of_state s slot =
           Some (ArchObjectCap (PageTableCap p (Some asid))))) and
    (\<lambda>s. ((\<exists>\<rhd> p) s \<longrightarrow> (\<forall>x. valid_pte (pt x) s)) \<and>
         (\<forall>ref. (ref \<unrhd> p) s \<longrightarrow>
            (\<forall>x p. pte_ref_pages (pt x) = Some p \<longrightarrow>
                   (\<exists>p' cap. caps_of_state s p' = Some cap \<and>
                        p \<in> obj_refs cap \<and>
                        vs_cap_ref cap =
                        Some (VSRef (ucast x) (Some APageTable) # ref)))))\<rbrace>
  set_pt p pt \<lbrace>\<lambda>_. valid_arch_caps\<rbrace>" unfolding valid_arch_caps_def apply (rule hoare_pre) apply (wp set_pt_valid_vs_lookup) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps and valid_arch_state and valid_vspace_objs and (\<lambda>s. valid_caps (caps_of_state s) s) and (\<lambda>s. ((\<exists>slot. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE)) \<or> (\<forall>slot. \<exists>asid. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p (Some asid))))) and (\<lambda>s. ((\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s)) \<and> (\<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<forall>x p. pte_ref_pages (pt x) = Some p \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref)))))\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) and valid_arch_state and valid_vspace_objs and (\<lambda>s. valid_caps (caps_of_state s) s) and (\<lambda>s. ((\<exists>slot. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE)) \<or> (\<forall>slot. \<exists>asid. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p (Some asid))))) and (\<lambda>s. ((\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s)) \<and> (\<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<forall>x p. pte_ref_pages (pt x) = Some p \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref)))))\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s))\<rbrace>
 2. \<And>s. (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) and valid_arch_state and valid_vspace_objs and (\<lambda>s. valid_caps (caps_of_state s) s) and (\<lambda>s. ((\<exists>slot. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE)) \<or> (\<forall>slot. \<exists>asid. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p (Some asid))))) and (\<lambda>s. ((\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s)) \<and> (\<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<forall>x p. pte_ref_pages (pt x) = Some p \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref)))))) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) and valid_arch_state and valid_vspace_objs and (\<lambda>s. valid_caps (caps_of_state s) s) and (\<lambda>s. ((\<exists>slot. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE)) \<or> (\<forall>slot. \<exists>asid. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p (Some asid))))) and (\<lambda>s. ((\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s)) \<and> (\<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<forall>x p. pte_ref_pages (pt x) = Some p \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref)))))) s \<Longrightarrow> (valid_vs_lookup s \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> ((\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s)) \<and> (\<forall>ref. (ref \<unrhd> p) s \<longrightarrow> (\<forall>x p. pte_ref_pages (pt x) = Some p \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref))))) \<and> (valid_table_caps and (\<lambda>s. valid_caps (caps_of_state s) s) and (\<lambda>s. ((\<exists>slot. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> pt = (\<lambda>x. InvalidPTE)) \<or> (\<forall>slot. \<exists>asid. caps_of_state s slot = Some (ArchObjectCap (PageTableCap p (Some asid)))))) s \<and> unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s) proof (prove)
goal:
No subgoals!