theory ArchVSpace_AI

lemma store_pte_unmap_page:
  "\<lbrace>(\<lambda>s. \<exists>pt. ([VSRef (vaddr >> 20) (Some APageDirectory),
               VSRef (asid && mask asid_low_bits) (Some AASIDPool),
               VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> pt) s
     \<and> is_aligned pt pt_bits \<and> p = (pt + ((vaddr >> 12) && mask 8 << 2 )))\<rbrace>
     store_pte p InvalidPTE
   \<lbrace>\<lambda>rv s.\<not> ([VSRef ((vaddr >> 12) && mask 8) (Some APageTable),
             VSRef (vaddr >> 20) (Some APageDirectory),
             VSRef (asid && mask asid_low_bits) (Some AASIDPool),
             VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> pptr) s\<rbrace>" apply (simp add: store_pte_def set_pt_def set_object_def get_object_def) apply (wp get_object_wp) apply (clarsimp simp: obj_at_def fun_upd_def[symmetric] vs_lookup_pages_def vs_asid_refs_def) apply (drule vs_lookup_pages1_rtrancl_iterations) apply (clarsimp simp: vs_lookup_pages1_def vs_lookup_def vs_asid_refs_def) apply (drule vs_lookup1_rtrancl_iterations) apply (clarsimp simp: vs_lookup1_def obj_at_def split: if_split_asm) apply (clarsimp simp: vs_refs_pages_def)+ apply (thin_tac "(VSRef a (Some AASIDPool), b) \<in> c" for a b c) apply (clarsimp simp: graph_of_def
                     split: Structures_A.kernel_object.split_asm
                            arch_kernel_obj.splits
                            if_split_asm) apply (erule_tac P="a = c" for c in swap) apply (rule up_ucast_inj[where 'a=8 and 'b=32]) apply (subst ucast_ucast_len) apply (simp add: pt_bits_def pageBits_def
                         is_aligned_add_helper less_le_trans[OF ucast_less]
                         shiftl_less_t2n'[where m=8 and n=2, simplified]
                         shiftr_less_t2n'[where m=8 and n=2, simplified]
                         word_bits_def shiftl_shiftr_id)+ apply (clarsimp simp: graph_of_def vs_refs_def vs_refs_pages_def
                          pde_ref_def pde_ref_pages_def pte_ref_pages_def)+ apply (simp add: pt_bits_def pageBits_def
                   is_aligned_add_helper less_le_trans[OF ucast_less]
                   shiftl_less_t2n'[where m=8 and n=2, simplified]
                   shiftr_less_t2n'[where m=8 and n=2, simplified]
                   word_bits_def shiftl_shiftr_id)+ by (clarsimp   split: Structures_A.kernel_object.split_asm arch_kernel_obj.split_asm,
         clarsimp simp: pde_ref_def pte_ref_pages_def pde_ref_pages_def data_at_def
                        is_aligned_add_helper less_le_trans[OF ucast_less]
                        shiftl_less_t2n'[where m=8 and n=2, simplified]
                 dest!: graph_ofD ucast_up_inj[where 'a=10 (*asid_low_bits*)and 'b=32, simplified]
                        ucast_up_inj[where 'a=7 (*asid_high_bits*) and 'b=32, simplified]
                 split: if_split_asm  pde.splits pte.splits if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>pt. ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pt) s \<and> is_aligned pt pt_bits \<and> p = pt + ((vaddr >> 12) && mask 8 << 2)\<rbrace> store_pte p InvalidPTE \<lbrace>\<lambda>rv s. ([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pptr) \<notin> vs_lookup_pages s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>pt. ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pt) s \<and> is_aligned pt pt_bits \<and> p = pt + ((vaddr >> 12) && mask 8 << 2)\<rbrace> do pt <- get_pt (p && ~~ mask pt_bits);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh (p && ~~ mask pt_bits) = Some y);
return (the (kh (p && ~~ mask pt_bits)))
od;
y <- assert (a_type kobj = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE))))\<rparr>)
od \<lbrace>\<lambda>rv s. ([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pptr) \<notin> vs_lookup_pages s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>pt. ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pt) s \<and> is_aligned pt pt_bits \<and> p = pt + ((vaddr >> 12) && mask 8 << 2) \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> (\<exists>y. kheap s (p && ~~ mask pt_bits) = Some y) \<longrightarrow> a_type (the (kheap s (p && ~~ mask pt_bits))) = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE)))) \<longrightarrow> ([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pptr) \<notin> vs_lookup_pages (s\<lparr>kheap := (kheap s)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := InvalidPTE))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s pt pta aa ba. \<lbrakk>([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pt) s; is_aligned pt pt_bits; p = pt + ((vaddr >> 12) && mask 8 << 2); kheap s (pt + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (pt + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), [VSRef ((vaddr >> 12) && mask 8) (Some APageTable), VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pptr) \<in> (vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(pt + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (pt + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE))))\<rparr>))\<^sup>*; (aa, ba) \<in> graph_of (asid_table s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pt pta aa ba. \<lbrakk>([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pt) s; is_aligned pt pt_bits; p = pt + ((vaddr >> 12) && mask 8 << 2); kheap s (pt + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (pt + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, ba) \<in> graph_of (asid_table s); length (fst ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba)) \<le> length (fst ([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pptr)) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), [VSRef ((vaddr >> 12) && mask 8) (Some APageTable), VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pptr) \<in> vs_lookup_pages1 (s\<lparr>kheap := (kheap s)(pt + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (pt + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE))))\<rparr>) ^^ (length (fst ([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pptr)) - length (fst ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pt pta aa be bf bg ah bh ko koa kob. \<lbrakk>is_aligned pt pt_bits; p = pt + ((vaddr >> 12) && mask 8 << 2); kheap s (pt + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (pt + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (([VSRef (UCAST(7 \<rightarrow> 32) ah) None], bh), [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], pt) \<in> (vs_lookup1 s)\<^sup>*; (ah, bh) \<in> graph_of (asid_table s); ko_at ko bg (s\<lparr>kheap := (kheap s)(pt + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (pt + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE))))\<rparr>); ko_at koa be (s\<lparr>kheap := (kheap s)(pt + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (pt + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE))))\<rparr>); ko_at kob bf (s\<lparr>kheap := (kheap s)(pt + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (pt + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE))))\<rparr>); (VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pt pta aa be bf bg ah bh ko koa kob. \<lbrakk>is_aligned pt pt_bits; p = pt + ((vaddr >> 12) && mask 8 << 2); kheap s (pt + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (pt + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, bh) \<in> graph_of (asid_table s); ko_at ko bg (s\<lparr>kheap := (kheap s)(pt + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (pt + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE))))\<rparr>); ko_at koa be (s\<lparr>kheap := (kheap s)(pt + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (pt + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE))))\<rparr>); ko_at kob bf (s\<lparr>kheap := (kheap s)(pt + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (pt + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE))))\<rparr>); (VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) aa; length (fst ([VSRef (UCAST(7 \<rightarrow> 32) ah) None], bh)) \<le> length (fst ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], pt)) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) ah) None], bh), [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], pt) \<in> vs_lookup1 s ^^ (length (fst ([VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) aa) None], pt)) - length (fst ([VSRef (UCAST(7 \<rightarrow> 32) ah) None], bh)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (8 subgoals):
 1. \<And>s pta aa ah b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (vaddr >> 20) (Some APageDirectory), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 2. \<And>s pta aa bf ah kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (vaddr >> 20) (Some APageDirectory), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 3. \<And>s pta aa be ah koa b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 4. \<And>s pta aa be bf ah koa kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 5. \<And>s pta aa bg ah ko b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 6. \<And>s pta aa bf bg ah ko kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 7. \<And>s pta aa be bg ah ko koa b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 8. \<And>s pta aa be bf bg ah ko koa kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>s pta aa be bf ah koa kob b ba bb koc kod a. \<lbrakk>(VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> (case koa of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {}); (VSRef (vaddr >> 20) (Some APageDirectory), bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits) \<in> (case kob of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {}); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + (UCAST(8 \<rightarrow> 32) a << 2); kheap s (bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + (UCAST(8 \<rightarrow> 32) a << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); be \<noteq> bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah; (a, pptr) \<in> graph_of (pte_ref_pages \<circ> pta(UCAST(32 \<rightarrow> 8) (bb + (UCAST(8 \<rightarrow> 32) a << 2) && mask pt_bits >> 2) := InvalidPTE)); (vaddr >> 12) && mask 8 = UCAST(8 \<rightarrow> 32) a\<rbrakk> \<Longrightarrow> False
 2. \<And>s pta aa bg ah ko b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 3. \<And>s pta aa bf bg ah ko kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 4. \<And>s pta aa be bg ah ko koa b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 5. \<And>s pta aa be bf bg ah ko koa kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>s pta aa be bf ah koa kob b ba bb koc kod a. \<lbrakk>(VSRef (vaddr >> 20) (Some APageDirectory), bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits) \<in> (case kob of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {}); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + (UCAST(8 \<rightarrow> 32) a << 2); kheap s (bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + (UCAST(8 \<rightarrow> 32) a << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); be \<noteq> bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah; (a, pptr) \<in> graph_of (pte_ref_pages \<circ> pta(UCAST(32 \<rightarrow> 8) (bb + (UCAST(8 \<rightarrow> 32) a << 2) && mask pt_bits >> 2) := InvalidPTE)); (vaddr >> 12) && mask 8 = UCAST(8 \<rightarrow> 32) a\<rbrakk> \<Longrightarrow> False
 2. \<And>s pta aa bg ah ko b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 3. \<And>s pta aa bf bg ah ko kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 4. \<And>s pta aa be bg ah ko koa b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 5. \<And>s pta aa be bf bg ah ko koa kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>s pta aa be bf ah koa b ba bb koc kod a x3 ab. \<lbrakk>vaddr >> 20 = UCAST(12 \<rightarrow> 32) ab; (vaddr >> 12) && mask 8 = UCAST(8 \<rightarrow> 32) a; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + (UCAST(8 \<rightarrow> 32) a << 2); kheap s (bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + (UCAST(8 \<rightarrow> 32) a << 2) && mask pt_bits >> 2) := InvalidPTE)))); asid_table s aa = Some be; asid_table s ah = Some b; be \<noteq> bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits; kheap s bf = Some (ArchObj (PageDirectory x3)); kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah; a \<noteq> UCAST(32 \<rightarrow> 8) (bb + (UCAST(8 \<rightarrow> 32) a << 2) && mask pt_bits >> 2); pte_ref_pages (pta a) = Some pptr; ab \<notin> kernel_mapping_slots; pde_ref_pages (x3 ab) = Some (bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits)\<rbrakk> \<Longrightarrow> False
 2. \<And>s pta aa bg ah ko b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 3. \<And>s pta aa bf bg ah ko kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 4. \<And>s pta aa be bg ah ko koa b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 5. \<And>s pta aa be bf bg ah ko koa kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>s pta aa be bf ah koa b ba bb koc kod a x3 ab. \<lbrakk>vaddr >> 20 = UCAST(12 \<rightarrow> 32) ab; (vaddr >> 12) && mask 8 = UCAST(8 \<rightarrow> 32) a; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + (UCAST(8 \<rightarrow> 32) a << 2); kheap s (bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + (UCAST(8 \<rightarrow> 32) a << 2) && mask pt_bits >> 2) := InvalidPTE)))); asid_table s aa = Some be; asid_table s ah = Some b; be \<noteq> bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits; kheap s bf = Some (ArchObj (PageDirectory x3)); kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah; pte_ref_pages (pta a) = Some pptr; ab \<notin> kernel_mapping_slots; pde_ref_pages (x3 ab) = Some (bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits); \<not> False\<rbrakk> \<Longrightarrow> a = UCAST(32 \<rightarrow> 8) (bb + (UCAST(8 \<rightarrow> 32) a << 2) && mask pt_bits >> 2)
 2. \<And>s pta aa bg ah ko b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 3. \<And>s pta aa bf bg ah ko kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 4. \<And>s pta aa be bg ah ko koa b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 5. \<And>s pta aa be bf bg ah ko koa kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>s pta aa be bf ah koa b ba bb koc kod a x3 ab. \<lbrakk>vaddr >> 20 = UCAST(12 \<rightarrow> 32) ab; (vaddr >> 12) && mask 8 = UCAST(8 \<rightarrow> 32) a; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + (UCAST(8 \<rightarrow> 32) a << 2); kheap s (bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + (UCAST(8 \<rightarrow> 32) a << 2) && mask pt_bits >> 2) := InvalidPTE)))); asid_table s aa = Some be; asid_table s ah = Some b; be \<noteq> bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits; kheap s bf = Some (ArchObj (PageDirectory x3)); kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah; pte_ref_pages (pta a) = Some pptr; ab \<notin> kernel_mapping_slots; pde_ref_pages (x3 ab) = Some (bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits); \<not> False\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) a = UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (bb + (UCAST(8 \<rightarrow> 32) a << 2) && mask pt_bits >> 2))
 2. \<And>s pta aa be bf ah koa b ba bb koc kod a x3 ab. \<lbrakk>vaddr >> 20 = UCAST(12 \<rightarrow> 32) ab; (vaddr >> 12) && mask 8 = UCAST(8 \<rightarrow> 32) a; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + (UCAST(8 \<rightarrow> 32) a << 2); kheap s (bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + (UCAST(8 \<rightarrow> 32) a << 2) && mask pt_bits >> 2) := InvalidPTE)))); asid_table s aa = Some be; asid_table s ah = Some b; be \<noteq> bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits; kheap s bf = Some (ArchObj (PageDirectory x3)); kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah; pte_ref_pages (pta a) = Some pptr; ab \<notin> kernel_mapping_slots; pde_ref_pages (x3 ab) = Some (bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits); \<not> False\<rbrakk> \<Longrightarrow> LENGTH(8) \<le> LENGTH(32)
 3. \<And>s pta aa bg ah ko b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 4. \<And>s pta aa bf bg ah ko kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 5. \<And>s pta aa be bg ah ko koa b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 6. \<And>s pta aa be bf bg ah ko koa kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False proof (prove)
goal (7 subgoals):
 1. \<And>s pta aa be bf ah koa b ba bb koc kod a x3 ab. \<lbrakk>vaddr >> 20 = UCAST(12 \<rightarrow> 32) ab; (vaddr >> 12) && mask 8 = UCAST(8 \<rightarrow> 32) a; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + (UCAST(8 \<rightarrow> 32) a << 2); kheap s (bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + (UCAST(8 \<rightarrow> 32) a << 2) && mask pt_bits >> 2) := InvalidPTE)))); asid_table s aa = Some be; asid_table s ah = Some b; be \<noteq> bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits; kheap s bf = Some (ArchObj (PageDirectory x3)); kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah; pte_ref_pages (pta a) = Some pptr; ab \<notin> kernel_mapping_slots; pde_ref_pages (x3 ab) = Some (bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits); \<not> False\<rbrakk> \<Longrightarrow> bb + (UCAST(8 \<rightarrow> 32) a << 2) && mask pt_bits >> 2 < 2 ^ LENGTH(8)
 2. \<And>s pta aa be bf ah koa b ba bb koc kod a x3 ab. \<lbrakk>vaddr >> 20 = UCAST(12 \<rightarrow> 32) ab; (vaddr >> 12) && mask 8 = UCAST(8 \<rightarrow> 32) a; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + (UCAST(8 \<rightarrow> 32) a << 2); kheap s (bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + (UCAST(8 \<rightarrow> 32) a << 2) && mask pt_bits >> 2) := InvalidPTE)))); asid_table s aa = Some be; asid_table s ah = Some b; be \<noteq> bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits; kheap s bf = Some (ArchObj (PageDirectory x3)); kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah; pte_ref_pages (pta a) = Some pptr; ab \<notin> kernel_mapping_slots; pde_ref_pages (x3 ab) = Some (bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits); \<not> False\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) a = bb + (UCAST(8 \<rightarrow> 32) a << 2) && mask pt_bits >> 2
 3. \<And>s pta aa be bf ah koa b ba bb koc kod a x3 ab. \<lbrakk>vaddr >> 20 = UCAST(12 \<rightarrow> 32) ab; (vaddr >> 12) && mask 8 = UCAST(8 \<rightarrow> 32) a; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + (UCAST(8 \<rightarrow> 32) a << 2); kheap s (bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + (UCAST(8 \<rightarrow> 32) a << 2) && mask pt_bits >> 2) := InvalidPTE)))); asid_table s aa = Some be; asid_table s ah = Some b; be \<noteq> bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits; kheap s bf = Some (ArchObj (PageDirectory x3)); kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (UCAST(12 \<rightarrow> 32) ab) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah; pte_ref_pages (pta a) = Some pptr; ab \<notin> kernel_mapping_slots; pde_ref_pages (x3 ab) = Some (bb + (UCAST(8 \<rightarrow> 32) a << 2) && ~~ mask pt_bits); \<not> False\<rbrakk> \<Longrightarrow> LENGTH(8) \<le> LENGTH(32)
 4. \<And>s pta aa bg ah ko b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 5. \<And>s pta aa bf bg ah ko kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 6. \<And>s pta aa be bg ah ko koa b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 7. \<And>s pta aa be bf bg ah ko koa kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s pta aa bg ah ko b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask 10) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask 10 >> 2) := InvalidPTE)))); (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask 10 >> 2) := InvalidPTE)))); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb 10; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask 10) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask 10 >> 2) := InvalidPTE)))); (aa, bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask 10) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask 10; kheap s bg = Some ko; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 2. \<And>s pta aa bf bg ah ko kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 3. \<And>s pta aa be bg ah ko koa b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False
 4. \<And>s pta aa be bf bg ah ko koa kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> vs_refs_pages ko; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> vs_refs_pages koa; (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> vs_refs_pages kob; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); (aa, be) \<in> graph_of (asid_table s); (ah, b) \<in> graph_of (asid_table s); bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> vs_refs koc; (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> vs_refs kod; UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pta aa be bf bg ah ko koa kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> (case ko of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {}); (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> (case koa of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {}); (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> (case kob of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {}); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb pt_bits; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask pt_bits >> 2) := InvalidPTE)))); asid_table s aa = Some be; asid_table s ah = Some b; bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bg = Some ko; be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s be = Some koa; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask pt_bits; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> (case koc of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}); (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> (case kod of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}); UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pta aa be bf bg ah ko koa kob b ba bb koc kod. \<lbrakk>(VSRef ((vaddr >> 12) && mask 8) (Some APageTable), pptr) \<in> (case ko of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {}); (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), bf) \<in> (case koa of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {}); (VSRef (vaddr >> 20) (Some APageDirectory), bg) \<in> (case kob of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageTable pt) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), y)) ` graph_of (pte_ref_pages \<circ> pt) | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) | ArchObj (DataPage dev s) \<Rightarrow> {} | _ \<Rightarrow> {}); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ah; is_aligned bb 10; p = bb + ((vaddr >> 12) && mask 8 << 2); kheap s (bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask 10) = Some (ArchObj (PageTable pta)); a_type (ArchObj (PageTable pta)) = a_type (ArchObj (PageTable (pta(UCAST(32 \<rightarrow> 8) (bb + ((vaddr >> 12) && mask 8 << 2) && mask 10 >> 2) := InvalidPTE)))); asid_table s aa = Some be; asid_table s ah = Some b; bg \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask 10; kheap s bg = Some ko; be \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask 10; kheap s be = Some koa; bf \<noteq> bb + ((vaddr >> 12) && mask 8 << 2) && ~~ mask 10; kheap s bf = Some kob; kheap s b = Some koc; kheap s ba = Some kod; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), ba) \<in> (case koc of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}); (VSRef (vaddr >> 20) (Some APageDirectory), bb) \<in> (case kod of ArchObj (ASIDPool pool) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(10 \<rightarrow> 32) r) (Some AASIDPool), y)) ` graph_of pool | ArchObj (PageDirectory pd) \<Rightarrow> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x)) | ArchObj _ \<Rightarrow> {} | _ \<Rightarrow> {}); UCAST(7 \<rightarrow> 32) aa = UCAST(7 \<rightarrow> 32) ah\<rbrakk> \<Longrightarrow> False