theory ArchVSpace_AI

lemma mapM_swp_store_pte_invs[wp]:
  "\<lbrace>invs and (\<lambda>s. (\<exists>p\<in>set slots. (\<exists>\<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow>
                  valid_pte pte s) and
    (\<lambda>s. wellformed_pte pte) and
    (\<lambda>s. \<exists>slot. cte_wp_at
           (\<lambda>c. image (\<lambda>x. x && ~~ mask pt_bits) (set slots) \<subseteq> obj_refs c \<and>
                is_pt_cap c \<and> (pte = InvalidPTE \<or>
                               cap_asid c \<noteq> None)) slot s) and
   (\<lambda>s. \<forall>p\<in>set slots. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow>
              (\<forall>q. pte_ref_pages pte = Some q \<longrightarrow>
                   (\<exists>p' cap.
                       caps_of_state s p' = Some cap \<and>
                       q \<in> obj_refs cap \<and>
                       vs_cap_ref cap =
                       Some
                        (VSRef (p && mask pt_bits >> 2) (Some APageTable) #
                         ref))))\<rbrace>
     mapM (swp store_pte pte) slots \<lbrace>\<lambda>_. invs\<rbrace>" apply (rule hoare_post_imp) prefer 2 apply (rule mapM_wp') apply simp_all apply (wp mapM_wp' hoare_vcg_imp_lift hoare_vcg_ex_lift hoare_vcg_ball_lift
            hoare_vcg_all_lift hoare_vcg_imp_lift) apply clarsimp apply (fastforce simp: cte_wp_at_caps_of_state is_pt_cap_def cap_asid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. (\<exists>p\<in>set slots. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s) and (\<lambda>s. wellformed_pte pte) and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set slots \<subseteq> obj_refs c \<and> is_pt_cap c \<and> (pte = InvalidPTE \<or> cap_asid c \<noteq> None)) slot s) and (\<lambda>s. \<forall>p\<in>set slots. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>q. pte_ref_pages pte = Some q \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref))))\<rbrace> mapM (swp store_pte pte) slots \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. ?Q rv s \<Longrightarrow> invs s
 2. \<lbrace>invs and (\<lambda>s. (\<exists>p\<in>set slots. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s) and (\<lambda>s. wellformed_pte pte) and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set slots \<subseteq> obj_refs c \<and> is_pt_cap c \<and> (pte = InvalidPTE \<or> cap_asid c \<noteq> None)) slot s) and (\<lambda>s. \<forall>p\<in>set slots. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>q. pte_ref_pages pte = Some q \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref))))\<rbrace> mapM (swp store_pte pte) slots \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>invs and (\<lambda>s. (\<exists>p\<in>set slots. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s) and (\<lambda>s. wellformed_pte pte) and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set slots \<subseteq> obj_refs c \<and> is_pt_cap c \<and> (pte = InvalidPTE \<or> cap_asid c \<noteq> None)) slot s) and (\<lambda>s. \<forall>p\<in>set slots. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>q. pte_ref_pages pte = Some q \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref))))\<rbrace> mapM (swp store_pte pte) slots \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> invs s proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set slots \<Longrightarrow> \<lbrace>invs and (\<lambda>s. (\<exists>p\<in>set slots. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s) and (\<lambda>s. wellformed_pte pte) and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set slots \<subseteq> obj_refs c \<and> is_pt_cap c \<and> (pte = InvalidPTE \<or> cap_asid c \<noteq> None)) slot s) and (\<lambda>s. \<forall>p\<in>set slots. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>q. pte_ref_pages pte = Some q \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref))))\<rbrace> swp store_pte pte x \<lbrace>\<lambda>rv. invs and (\<lambda>s. (\<exists>p\<in>set slots. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s) and (\<lambda>s. wellformed_pte pte) and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set slots \<subseteq> obj_refs c \<and> is_pt_cap c \<and> (pte = InvalidPTE \<or> cap_asid c \<noteq> None)) slot s) and (\<lambda>s. \<forall>p\<in>set slots. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>q. pte_ref_pages pte = Some q \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref))))\<rbrace>
 2. \<And>rv s. (invs and (\<lambda>s. (\<exists>p\<in>set slots. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s) and (\<lambda>s. wellformed_pte pte) and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set slots \<subseteq> obj_refs c \<and> is_pt_cap c \<and> (pte = InvalidPTE \<or> cap_asid c \<noteq> None)) slot s) and (\<lambda>s. \<forall>p\<in>set slots. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>q. pte_ref_pages pte = Some q \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref))))) s \<Longrightarrow> invs s proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set slots \<Longrightarrow> \<lbrace>invs and (\<lambda>s. (\<exists>p\<in>set slots. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s) and (\<lambda>s. wellformed_pte pte) and (\<lambda>s. \<exists>a b. cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set slots \<subseteq> obj_refs c \<and> is_pt_cap c \<and> (pte = InvalidPTE \<or> (\<exists>y. cap_asid c = Some y))) (a, b) s) and (\<lambda>s. \<forall>p\<in>set slots. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>q. pte_ref_pages pte = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref))))\<rbrace> store_pte x pte \<lbrace>\<lambda>rv. invs and (\<lambda>s. (\<exists>p\<in>set slots. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s) and (\<lambda>s. wellformed_pte pte) and (\<lambda>s. \<exists>a b. cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set slots \<subseteq> obj_refs c \<and> is_pt_cap c \<and> (pte = InvalidPTE \<or> (\<exists>y. cap_asid c = Some y))) (a, b) s) and (\<lambda>s. \<forall>p\<in>set slots. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>q. pte_ref_pages pte = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref))))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>x \<in> set slots; (invs and (\<lambda>s. (\<exists>p\<in>set slots. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s) and (\<lambda>s. wellformed_pte pte) and (\<lambda>s. \<exists>a b. cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set slots \<subseteq> obj_refs c \<and> is_pt_cap c \<and> (pte = InvalidPTE \<or> (\<exists>y. cap_asid c = Some y))) (a, b) s) and (\<lambda>s. \<forall>p\<in>set slots. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>q. pte_ref_pages pte = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref))))) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (\<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s) and (\<lambda>s. wellformed_pte pte) and (\<lambda>s. \<exists>slot asid. caps_of_state s slot = Some (ArchObjectCap (PageTableCap (x && ~~ mask pt_bits) asid)) \<and> (pte = InvalidPTE \<or> asid \<noteq> None)) and (\<lambda>s. \<forall>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>q. pte_ref_pages pte = Some q \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (x && mask pt_bits >> 2) (Some APageTable) # ref))))) s \<and> (\<not> (\<exists>p\<in>set slots. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<or> valid_pte pte s) \<and> wellformed_pte pte \<and> (\<exists>x xa. cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set slots \<subseteq> obj_refs c \<and> is_pt_cap c \<and> (pte = InvalidPTE \<or> (\<exists>y. cap_asid c = Some y))) (x, xa) s) \<and> (\<forall>x\<in>set slots. \<forall>xa. (xa, x && ~~ mask pt_bits) \<notin> vs_lookup s \<or> (\<forall>xb. pte_ref_pages pte \<noteq> Some xb \<or> (\<exists>xc xd xe. caps_of_state s (xc, xd) = Some xe \<and> xb \<in> obj_refs xe \<and> vs_cap_ref xe = Some (VSRef (x && mask pt_bits >> 2) (Some APageTable) # xa)))) proof (prove)
goal (1 subgoal):
 1. \<And>x s a b. \<lbrakk>x \<in> set slots; invs s; (\<exists>p\<in>set slots. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<forall>p\<in>set slots. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>q. pte_ref_pages pte = Some q \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref))); cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set slots \<subseteq> obj_refs c \<and> is_pt_cap c \<and> (pte = InvalidPTE \<or> (\<exists>y. cap_asid c = Some y))) (a, b) s\<rbrakk> \<Longrightarrow> ((\<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s) \<and> (\<exists>a b asid. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (x && ~~ mask pt_bits) asid)) \<and> (pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)))) \<and> ((\<forall>p\<in>set slots. \<forall>ref. (ref, p && ~~ mask pt_bits) \<notin> vs_lookup s) \<or> valid_pte pte s) proof (prove)
goal:
No subgoals!