theory ArchAcc_AI

lemma store_pte_invs [wp]:
  "\<lbrace>invs and (\<lambda>s. (\<exists>\<rhd>(p && ~~ 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 (p && ~~ mask pt_bits) asid)) \<and>
         (pte = InvalidPTE \<or> asid \<noteq> None)) and
    (\<lambda>s. \<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>
  store_pte p pte \<lbrace>\<lambda>_. invs\<rbrace>" apply (simp add: store_pte_def) apply (wp dmo_invs set_pt_invs) apply clarsimp apply (intro conjI) apply (drule invs_valid_objs) apply (fastforce simp: valid_objs_def dom_def obj_at_def valid_obj_def arch_valid_obj_def) apply clarsimp apply (drule (1) valid_vspace_objsD, fastforce) apply simp apply (thin_tac "All _") apply (rule exI)+ apply (rule conjI, assumption) subgoal premises prems for \<dots> asid proof (cases asid) case (Some a) from this show ?thesis by fastforce next case None from this prems show ?thesis apply clarsimp apply (rule ext) apply clarsimp apply (frule invs_pd_caps) apply (clarsimp simp add: valid_table_caps_def simp del: HOL.imp_disjL) apply (spec "p && ~~ mask pt_bits") apply (drule spec)+ apply (erule impE, assumption) by (simp add: is_pt_cap_def cap_asid_def empty_table_def obj_at_def) qed apply (clarsimp simp: obj_at_def) apply (intro impI conjI allI) apply (drule (2) vs_lookup_pages_pt_eq[OF invs_vspace_objs invs_ran_asid_table,
                                          THEN iffD1, rotated -1]) apply (clarsimp simp: obj_at_def a_type_simps) apply (drule spec, erule impE, assumption)+ apply (erule exEI)+ apply clarsimp apply (rule sym) apply (rule ucast_ucast_len) apply (rule shiftr_less_t2n) using and_mask_less'[of 10 p] apply (simp add: pt_bits_def pageBits_def) subgoal for \<dots> pa apply (thin_tac "All _", thin_tac "_ \<longrightarrow> _", thin_tac "_ \<or> _") apply (frule invs_valid_vs_lookup) apply (simp add: valid_vs_lookup_def) apply (spec pa) apply (drule spec, erule impE) apply (erule vs_lookup_pages_step) by (fastforce simp: vs_lookup_pages1_def obj_at_def
                          vs_refs_pages_def graph_of_def image_def) simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. (\<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 asid. caps_of_state s slot = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)) \<and> (pte = InvalidPTE \<or> asid \<noteq> None)) and (\<lambda>s. \<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> store_pte p pte \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. (\<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 asid. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)) \<and> (pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)))) and (\<lambda>s. \<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> do pt <- get_pt (p && ~~ mask pt_bits);
set_pt (p && ~~ mask pt_bits) (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))
od \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and (\<lambda>s. (\<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 asid. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)) \<and> (pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)))) and (\<lambda>s. \<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 \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> (invs and (\<lambda>s. \<forall>i. wellformed_pte ((pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) i)) and (\<lambda>s. (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_vspace_obj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))) s) and (\<lambda>s. \<exists>slot asid. caps_of_state s slot = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)) \<and> (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> asid \<noteq> None)) and (\<lambda>s. \<forall>ref. (ref \<unrhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>x pa. pte_ref_pages ((pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) x) = Some pa \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref))))) s proof (prove)
goal (1 subgoal):
 1. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> (\<forall>i. i \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> wellformed_pte (pt i)) \<and> ((\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> (\<forall>x. x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> valid_pte (pt x) s)) \<and> (\<exists>a b asid. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)) \<and> (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b)))) \<and> (\<forall>ref. (ref \<unrhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>x. (x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>pa. pte_ref_pages pte = Some pa \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) (Some APageTable) # ref)))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>p. pte_ref_pages (pt x) = Some p \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref)))))) proof (prove)
goal (4 subgoals):
 1. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> \<forall>i. i \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> wellformed_pte (pt i)
 2. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> (\<forall>x. x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> valid_pte (pt x) s)
 3. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> \<exists>a b asid. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)) \<and> (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b)))
 4. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> \<forall>ref. (ref \<unrhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>x. (x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>pa. pte_ref_pages pte = Some pa \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) (Some APageTable) # ref)))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>p. pte_ref_pages (pt x) = Some p \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref))))) proof (prove)
goal (4 subgoals):
 1. \<And>s pt a b asid. \<lbrakk>(\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s; valid_objs s\<rbrakk> \<Longrightarrow> \<forall>i. i \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> wellformed_pte (pt i)
 2. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> (\<forall>x. x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> valid_pte (pt x) s)
 3. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> \<exists>a b asid. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)) \<and> (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b)))
 4. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> \<forall>ref. (ref \<unrhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>x. (x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>pa. pte_ref_pages pte = Some pa \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) (Some APageTable) # ref)))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>p. pte_ref_pages (pt x) = Some p \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref))))) proof (prove)
goal (3 subgoals):
 1. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> (\<forall>x. x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> valid_pte (pt x) s)
 2. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> \<exists>a b asid. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)) \<and> (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b)))
 3. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> \<forall>ref. (ref \<unrhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>x. (x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>pa. pte_ref_pages pte = Some pa \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) (Some APageTable) # ref)))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>p. pte_ref_pages (pt x) = Some p \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref))))) proof (prove)
goal (3 subgoals):
 1. \<And>s pt a b asid ref x. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s; (ref \<rhd> (p && ~~ mask pt_bits)) s; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> valid_pte (pt x) s
 2. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> \<exists>a b asid. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)) \<and> (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b)))
 3. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> \<forall>ref. (ref \<unrhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>x. (x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>pa. pte_ref_pages pte = Some pa \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) (Some APageTable) # ref)))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>p. pte_ref_pages (pt x) = Some p \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref))))) proof (prove)
goal (3 subgoals):
 1. \<And>s pt a b asid ref x. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_vspace_obj (PageTable pt) s\<rbrakk> \<Longrightarrow> valid_pte (pt x) s
 2. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> \<exists>a b asid. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)) \<and> (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b)))
 3. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> \<forall>ref. (ref \<unrhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>x. (x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>pa. pte_ref_pages pte = Some pa \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) (Some APageTable) # ref)))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>p. pte_ref_pages (pt x) = Some p \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref))))) proof (prove)
goal (2 subgoals):
 1. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> \<exists>a b asid. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)) \<and> (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b)))
 2. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> \<forall>ref. (ref \<unrhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>x. (x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>pa. pte_ref_pages pte = Some pa \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) (Some APageTable) # ref)))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>p. pte_ref_pages (pt x) = Some p \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref))))) proof (prove)
goal (2 subgoals):
 1. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> \<exists>a b asid. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)) \<and> (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b)))
 2. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> \<forall>ref. (ref \<unrhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>x. (x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>pa. pte_ref_pages pte = Some pa \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) (Some APageTable) # ref)))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>p. pte_ref_pages (pt x) = Some p \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref))))) proof (prove)
goal (2 subgoals):
 1. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> caps_of_state s (?a132 s pt a b asid, ?b134 s pt a b asid) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) (?asid136 s pt a b asid))) \<and> (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>aa ba. ?asid136 s pt a b asid = Some (aa, ba)))
 2. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> \<forall>ref. (ref \<unrhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>x. (x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>pa. pte_ref_pages pte = Some pa \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) (Some APageTable) # ref)))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>p. pte_ref_pages (pt x) = Some p \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref))))) proof (prove)
goal (2 subgoals):
 1. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b))
 2. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> \<forall>ref. (ref \<unrhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>x. (x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>pa. pte_ref_pages pte = Some pa \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) (Some APageTable) # ref)))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>p. pte_ref_pages (pt x) = Some p \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref))))) proof (prove)
goal (1 subgoal):
 1. pt_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b)) proof (state)
goal (2 subgoals):
 1. asid = None \<Longrightarrow> pt_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b))
 2. \<And>a. asid = Some a \<Longrightarrow> pt_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b)) proof (state)
this:
asid = Some a

goal (2 subgoals):
 1. asid = None \<Longrightarrow> pt_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b))
 2. \<And>a. asid = Some a \<Longrightarrow> pt_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b)) proof (chain)
picking this:
asid = Some a proof (prove)
using this:
asid = Some a

goal (1 subgoal):
 1. pt_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b)) proof (state)
this:
pt_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b))

goal (1 subgoal):
 1. asid = None \<Longrightarrow> pt_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b)) proof (state)
goal (1 subgoal):
 1. asid = None \<Longrightarrow> pt_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b)) proof (state)
this:
asid = None

goal (1 subgoal):
 1. asid = None \<Longrightarrow> pt_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b)) proof (chain)
picking this:
asid = None
invs s_
(\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s_) \<longrightarrow> valid_pte pte s_
wellformed_pte pte
caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid))
pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b))
ako_at (PageTable pt_) (p && ~~ mask pt_bits) s_ proof (prove)
using this:
asid = None
invs s_
(\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s_) \<longrightarrow> valid_pte pte s_
wellformed_pte pte
caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid))
pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b))
ako_at (PageTable pt_) (p && ~~ mask pt_bits) s_

goal (1 subgoal):
 1. pt_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>asid = None; invs s_; caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) None)); pte = InvalidPTE; ako_at (PageTable pt_) (p && ~~ mask pt_bits) s_\<rbrakk> \<Longrightarrow> pt_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE) = (\<lambda>x. InvalidPTE) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>asid = None; invs s_; caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) None)); pte = InvalidPTE; ako_at (PageTable pt_) (p && ~~ mask pt_bits) s_\<rbrakk> \<Longrightarrow> (pt_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE)) x = InvalidPTE proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>asid = None; invs s_; caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) None)); pte = InvalidPTE; ako_at (PageTable pt_) (p && ~~ mask pt_bits) s_; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> pt_ x = InvalidPTE proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>asid = None; invs s_; caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) None)); pte = InvalidPTE; ako_at (PageTable pt_) (p && ~~ mask pt_bits) s_; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); valid_table_caps s_\<rbrakk> \<Longrightarrow> pt_ x = InvalidPTE proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>asid = None; invs s_; caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) None)); pte = InvalidPTE; ako_at (PageTable pt_) (p && ~~ mask pt_bits) s_; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); \<forall>r a b cap. caps_of_state s_ (a, b) = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s_)))) r s_\<rbrakk> \<Longrightarrow> pt_ x = InvalidPTE proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>asid = None; invs s_; caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) None)); pte = InvalidPTE; ako_at (PageTable pt_) (p && ~~ mask pt_bits) s_; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); \<forall>a b cap. caps_of_state s_ (a, b) = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> p && ~~ mask pt_bits \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s_)))) (p && ~~ mask pt_bits) s_\<rbrakk> \<Longrightarrow> pt_ x = InvalidPTE proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>asid = None; invs s_; caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) None)); pte = InvalidPTE; ako_at (PageTable pt_) (p && ~~ mask pt_bits) s_; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); caps_of_state s_ (?a18 x, ?b20 x) = Some (?cap22 x) \<longrightarrow> is_pd_cap (?cap22 x) \<or> is_pt_cap (?cap22 x) \<longrightarrow> cap_asid (?cap22 x) = None \<longrightarrow> p && ~~ mask pt_bits \<in> obj_refs (?cap22 x) \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s_)))) (p && ~~ mask pt_bits) s_\<rbrakk> \<Longrightarrow> pt_ x = InvalidPTE proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>asid = None; invs s_; caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) None)); pte = InvalidPTE; ako_at (PageTable pt_) (p && ~~ mask pt_bits) s_; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); is_pd_cap (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) None)) \<or> is_pt_cap (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) None)) \<longrightarrow> cap_asid (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) None)) = None \<longrightarrow> p && ~~ mask pt_bits \<in> obj_refs (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) None)) \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s_)))) (p && ~~ mask pt_bits) s_\<rbrakk> \<Longrightarrow> pt_ x = InvalidPTE proof (state)
this:
pt_(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte) = (\<lambda>x. InvalidPTE) \<or> (\<exists>a b. asid = Some (a, b))

goal:
No subgoals! proof (prove)
goal (1 subgoal):
 1. \<And>s pt a b asid. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); ako_at (PageTable pt) (p && ~~ mask pt_bits) s\<rbrakk> \<Longrightarrow> \<forall>ref. (ref \<unrhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>x. (x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>pa. pte_ref_pages pte = Some pa \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) (Some APageTable) # ref)))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>p. pte_ref_pages (pt x) = Some p \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref))))) proof (prove)
goal (1 subgoal):
 1. \<And>s pt a b asid ref x. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); (ref \<unrhd> (p && ~~ mask pt_bits)) s\<rbrakk> \<Longrightarrow> (x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>pa. pte_ref_pages pte = Some pa \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) (Some APageTable) # ref)))) \<and> (x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) \<longrightarrow> (\<forall>p. pte_ref_pages (pt x) = Some p \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref)))) proof (prove)
goal (2 subgoals):
 1. \<And>s pt a b asid ref x pa. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); (ref \<unrhd> (p && ~~ mask pt_bits)) s; x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages pte = Some pa\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) (Some APageTable) # ref)
 2. \<And>s pt a b asid ref x pa. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); (ref \<unrhd> (p && ~~ mask pt_bits)) s; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt x) = Some pa\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref) proof (prove)
goal (3 subgoals):
 1. \<And>s pt a b asid ref x pa. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages pte = Some pa\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) (p && ~~ mask pt_bits) s
 2. \<And>s pt a b asid ref x pa. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages pte = Some pa; (ref \<rhd> (p && ~~ mask pt_bits)) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) (Some APageTable) # ref)
 3. \<And>s pt a b asid ref x pa. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); (ref \<unrhd> (p && ~~ mask pt_bits)) s; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt x) = Some pa\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref) proof (prove)
goal (2 subgoals):
 1. \<And>s pt a b asid ref x pa. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages pte = Some pa; (ref \<rhd> (p && ~~ mask pt_bits)) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) (Some APageTable) # ref)
 2. \<And>s pt a b asid ref x pa. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); (ref \<unrhd> (p && ~~ mask pt_bits)) s; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt x) = Some pa\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref) proof (prove)
goal (2 subgoals):
 1. \<And>s pt a b asid ref x pa. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages pte = Some pa; (ref \<rhd> (p && ~~ mask pt_bits)) s; \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) (Some APageTable) # ref)
 2. \<And>s pt a b asid ref x pa. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); (ref \<unrhd> (p && ~~ mask pt_bits)) s; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt x) = Some pa\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref) proof (prove)
goal (2 subgoals):
 1. \<And>s pt a b asid ref x pa xa xb xc. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); x = UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages pte = Some pa; (ref \<rhd> (p && ~~ mask pt_bits)) s; caps_of_state s (xa, xb) = Some xc \<and> pa \<in> obj_refs xc \<and> vs_cap_ref xc = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref)\<rbrakk> \<Longrightarrow> caps_of_state s (xa, xb) = Some xc \<and> pa \<in> obj_refs xc \<and> vs_cap_ref xc = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) (Some APageTable) # ref)
 2. \<And>s pt a b asid ref x pa. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); (ref \<unrhd> (p && ~~ mask pt_bits)) s; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt x) = Some pa\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref) proof (prove)
goal (2 subgoals):
 1. \<And>s pt a b asid ref pa xa xb xc. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_ref_pages pte = Some pa; (ref \<rhd> (p && ~~ mask pt_bits)) s; caps_of_state s (xa, xb) = Some xc; pa \<in> obj_refs xc; vs_cap_ref xc = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref)\<rbrakk> \<Longrightarrow> p && mask pt_bits >> 2 = UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))
 2. \<And>s pt a b asid ref x pa. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); (ref \<unrhd> (p && ~~ mask pt_bits)) s; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt x) = Some pa\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref) proof (prove)
goal (2 subgoals):
 1. \<And>s pt a b asid ref pa xa xb xc. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_ref_pages pte = Some pa; (ref \<rhd> (p && ~~ mask pt_bits)) s; caps_of_state s (xa, xb) = Some xc; pa \<in> obj_refs xc; vs_cap_ref xc = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref)\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) = p && mask pt_bits >> 2
 2. \<And>s pt a b asid ref x pa. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); (ref \<unrhd> (p && ~~ mask pt_bits)) s; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt x) = Some pa\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref) proof (prove)
goal (2 subgoals):
 1. \<And>s pt a b asid ref pa xa xb xc. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_ref_pages pte = Some pa; (ref \<rhd> (p && ~~ mask pt_bits)) s; caps_of_state s (xa, xb) = Some xc; pa \<in> obj_refs xc; vs_cap_ref xc = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref)\<rbrakk> \<Longrightarrow> p && mask pt_bits >> 2 < 2 ^ LENGTH(8)
 2. \<And>s pt a b asid ref x pa. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); (ref \<unrhd> (p && ~~ mask pt_bits)) s; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt x) = Some pa\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref) proof (prove)
goal (2 subgoals):
 1. \<And>s pt a b asid ref pa xa xb xc. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_ref_pages pte = Some pa; (ref \<rhd> (p && ~~ mask pt_bits)) s; caps_of_state s (xa, xb) = Some xc; pa \<in> obj_refs xc; vs_cap_ref xc = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref)\<rbrakk> \<Longrightarrow> p && mask pt_bits < 2 ^ (2 + LENGTH(8))
 2. \<And>s pt a b asid ref x pa. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); (ref \<unrhd> (p && ~~ mask pt_bits)) s; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt x) = Some pa\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref) proof (prove)
using this:
10 < LENGTH(32) \<Longrightarrow> p && mask 10 < 2 ^ 10

goal (2 subgoals):
 1. \<And>s pt a b asid ref pa xa xb xc. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pte_ref_pages pte = Some pa; (ref \<rhd> (p && ~~ mask pt_bits)) s; caps_of_state s (xa, xb) = Some xc; pa \<in> obj_refs xc; vs_cap_ref xc = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref)\<rbrakk> \<Longrightarrow> p && mask pt_bits < 2 ^ (2 + LENGTH(8))
 2. \<And>s pt a b asid ref x pa. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); (ref \<unrhd> (p && ~~ mask pt_bits)) s; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt x) = Some pa\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref) proof (prove)
goal (1 subgoal):
 1. \<And>s pt a b asid ref x pa. \<lbrakk>invs s; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s; wellformed_pte pte; \<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))); caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid)); pte = InvalidPTE \<or> (\<exists>a b. asid = Some (a, b)); kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); (ref \<unrhd> (p && ~~ mask pt_bits)) s; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt x) = Some pa\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable) # ref) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s_; (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s_) \<longrightarrow> valid_pte pte s_; wellformed_pte pte; \<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))); caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid_)); pte = InvalidPTE \<or> (\<exists>a b. asid_ = Some (a, b)); kheap s_ (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt_)); (ref_ \<unrhd> (p && ~~ mask pt_bits)) s_; x_ \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt_ x_) = Some pa\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s_ (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x_) (Some APageTable) # ref_) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s_; wellformed_pte pte; caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid_)); kheap s_ (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt_)); (ref_ \<unrhd> (p && ~~ mask pt_bits)) s_; x_ \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt_ x_) = Some pa\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s_ (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x_) (Some APageTable) # ref_) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s_; wellformed_pte pte; caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid_)); kheap s_ (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt_)); (ref_ \<unrhd> (p && ~~ mask pt_bits)) s_; x_ \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt_ x_) = Some pa; valid_vs_lookup s_\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s_ (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x_) (Some APageTable) # ref_) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s_; wellformed_pte pte; caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid_)); kheap s_ (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt_)); (ref_ \<unrhd> (p && ~~ mask pt_bits)) s_; x_ \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt_ x_) = Some pa; \<forall>p ref. (ref \<unrhd> p) s_ \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s_ (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s_ (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x_) (Some APageTable) # ref_) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s_; wellformed_pte pte; caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid_)); kheap s_ (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt_)); (ref_ \<unrhd> (p && ~~ mask pt_bits)) s_; x_ \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt_ x_) = Some pa; \<forall>ref. (ref \<unrhd> pa) s_ \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s_ (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s_ (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x_) (Some APageTable) # ref_) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s_; wellformed_pte pte; caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid_)); kheap s_ (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt_)); (ref_ \<unrhd> (p && ~~ mask pt_bits)) s_; x_ \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt_ x_) = Some pa\<rbrakk> \<Longrightarrow> (?ref20 \<unrhd> pa) s_
 2. \<lbrakk>invs s_; wellformed_pte pte; caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid_)); kheap s_ (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt_)); (ref_ \<unrhd> (p && ~~ mask pt_bits)) s_; x_ \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt_ x_) = Some pa; ?ref20 \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s_ (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some ?ref20)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s_ (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x_) (Some APageTable) # ref_) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s_; wellformed_pte pte; caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid_)); kheap s_ (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt_)); x_ \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt_ x_) = Some pa\<rbrakk> \<Longrightarrow> ((ref_, p && ~~ mask pt_bits), ?ref20, pa) \<in> vs_lookup_pages1 s_
 2. \<lbrakk>invs s_; wellformed_pte pte; caps_of_state s_ (a_, b_) = Some (ArchObjectCap (PageTableCap (p && ~~ mask pt_bits) asid_)); kheap s_ (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt_)); (ref_ \<unrhd> (p && ~~ mask pt_bits)) s_; x_ \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); pte_ref_pages (pt_ x_) = Some pa; ?ref20 \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s_ (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some ?ref20)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s_ (a, b) = Some cap \<and> pa \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) x_) (Some APageTable) # ref_) proof (prove)
goal:
No subgoals!