theory ArchVSpace_AI

lemma store_pde_unmap_pt:
  "\<lbrace>[VSRef (asid && mask asid_low_bits) (Some AASIDPool),
            VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> pd
        and K (is_aligned pd pd_bits)\<rbrace>
     store_pde (pd + (vaddr >> 20 << 2)) InvalidPDE
   \<lbrace>\<lambda>rv s.
        \<not> ([VSRef (vaddr >> 20) (Some APageDirectory),
            VSRef (asid && mask asid_low_bits) (Some AASIDPool),
            VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> pt) s\<rbrace>" apply (simp add: store_pde_def set_pd_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: obj_at_def fun_upd_def[symmetric]) apply (clarsimp simp: vs_lookup_def vs_asid_refs_def
                 dest!: graph_ofD vs_lookup1_rtrancl_iterations) apply (clarsimp simp: vs_lookup1_def obj_at_def vs_refs_def
                 dest!: graph_ofD
                 split: if_split_asm
                        Structures_A.kernel_object.split_asm
                        arch_kernel_obj.split_asm) apply (simp add: pde_ref_def) apply (simp_all add: pd_shifting_again pd_shifting_again2
                        pd_casting_shifting word_size) apply (simp add: up_ucast_inj_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>[VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd and K (is_aligned pd pd_bits)\<rbrace> store_pde (pd + (vaddr >> 20 << 2)) InvalidPDE \<lbrace>\<lambda>rv s. ([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], pt) \<notin> vs_lookup s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>[VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd and (\<lambda>y. is_aligned pd pd_bits)\<rbrace> do pda <- get_pd (pd + (vaddr >> 20 << 2) && ~~ mask pd_bits);
kobj <- get_object (pd + (vaddr >> 20 << 2) && ~~ mask pd_bits);
y <- assert (a_type kobj = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (pd + (vaddr >> 20 << 2) && mask pd_bits >> 2) := InvalidPDE)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(pd + (vaddr >> 20 << 2) && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (pd + (vaddr >> 20 << 2) && mask pd_bits >> 2) := InvalidPDE))))\<rparr>)
od \<lbrace>\<lambda>rv s. ([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], pt) \<notin> vs_lookup s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd and (\<lambda>y. is_aligned pd pd_bits)) s \<Longrightarrow> \<forall>pda. ako_at (PageDirectory pda) (pd + (vaddr >> 20 << 2) && ~~ mask pd_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (pd + (vaddr >> 20 << 2) && ~~ mask pd_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (pd + (vaddr >> 20 << 2) && mask pd_bits >> 2) := InvalidPDE)))) \<longrightarrow> ([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], pt) \<notin> vs_lookup (s\<lparr>kheap := (kheap s)(pd + (vaddr >> 20 << 2) && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (pd + (vaddr >> 20 << 2) && mask pd_bits >> 2) := InvalidPDE))))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s pda. \<lbrakk>([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; is_aligned pd pd_bits; kheap s (pd + (vaddr >> 20 << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (pd + (vaddr >> 20 << 2) && mask pd_bits >> 2) := InvalidPDE)))); ([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\<lparr>kheap := (kheap s)(pd + (vaddr >> 20 << 2) && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (pd + (vaddr >> 20 << 2) && mask pd_bits >> 2) := InvalidPDE))))\<rparr>)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pda ab bb ac b aa ba. \<lbrakk>is_aligned pd pd_bits; kheap s (pd + (vaddr >> 20 << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (pd + (vaddr >> 20 << 2) && mask pd_bits >> 2) := InvalidPDE)))); asid_table s ab = Some bb; asid_table s ac = Some b; (([VSRef (UCAST(7 \<rightarrow> 32) ab) None], bb), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<in> vs_lookup1 s; (([VSRef (UCAST(7 \<rightarrow> 32) ac) None], b), aa, ba) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(pd + (vaddr >> 20 << 2) && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (pd + (vaddr >> 20 << 2) && mask pd_bits >> 2) := InvalidPDE))))\<rparr>); ((aa, ba), [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], pt) \<in> vs_lookup1 (s\<lparr>kheap := (kheap s)(pd + (vaddr >> 20 << 2) && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (pd + (vaddr >> 20 << 2) && mask pd_bits >> 2) := InvalidPDE))))\<rparr>)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s pda ab bb ac b x1 x1a a ad ae. \<lbrakk>x1a ae = Some (pd + (UCAST(12 \<rightarrow> 32) ad << 2) && ~~ mask pd_bits); UCAST(10 \<rightarrow> 32) ae = UCAST(10 \<rightarrow> 32) a; vaddr >> 20 = UCAST(12 \<rightarrow> 32) ad; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a; UCAST(7 \<rightarrow> 32) ab = UCAST(7 \<rightarrow> 32) ac; is_aligned pd pd_bits; kheap s (pd + (UCAST(12 \<rightarrow> 32) ad << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(ad := InvalidPDE)))); asid_table s ab = Some bb; asid_table s ac = Some b; b \<noteq> pd + (UCAST(12 \<rightarrow> 32) ad << 2) && ~~ mask pd_bits; kheap s bb = Some (ArchObj (ASIDPool x1)); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ac; kheap s b = Some (ArchObj (ASIDPool x1a)); x1 a = Some pd; ad \<notin> kernel_mapping_slots; ad = UCAST(32 \<rightarrow> 12) (pd + (UCAST(12 \<rightarrow> 32) ad << 2) && mask pd_bits >> 2); pde_ref InvalidPDE = Some pt\<rbrakk> \<Longrightarrow> False
 2. \<And>s pda ab bb ac b x1 x1a a ad ae. \<lbrakk>x1a ae = Some (pd + (UCAST(12 \<rightarrow> 32) ad << 2) && ~~ mask pd_bits); UCAST(10 \<rightarrow> 32) ae = UCAST(10 \<rightarrow> 32) a; vaddr >> 20 = UCAST(12 \<rightarrow> 32) ad; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a; UCAST(7 \<rightarrow> 32) ab = UCAST(7 \<rightarrow> 32) ac; is_aligned pd pd_bits; kheap s (pd + (UCAST(12 \<rightarrow> 32) ad << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (pd + (UCAST(12 \<rightarrow> 32) ad << 2) && mask pd_bits >> 2) := InvalidPDE)))); asid_table s ab = Some bb; asid_table s ac = Some b; b \<noteq> pd + (UCAST(12 \<rightarrow> 32) ad << 2) && ~~ mask pd_bits; kheap s bb = Some (ArchObj (ASIDPool x1)); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ac; kheap s b = Some (ArchObj (ASIDPool x1a)); x1 a = Some pd; ad \<notin> kernel_mapping_slots; ad \<noteq> UCAST(32 \<rightarrow> 12) (pd + (UCAST(12 \<rightarrow> 32) ad << 2) && mask pd_bits >> 2); pde_ref (pda ad) = Some pt\<rbrakk> \<Longrightarrow> False
 3. \<And>s pda ab bb ac b x1 x3 x1a a ad ae be. \<lbrakk>x1a ae = Some be; UCAST(10 \<rightarrow> 32) ae = UCAST(10 \<rightarrow> 32) a; vaddr >> 20 = UCAST(12 \<rightarrow> 32) ad; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a; kheap s be = Some (ArchObj (PageDirectory x3)); UCAST(7 \<rightarrow> 32) ab = UCAST(7 \<rightarrow> 32) ac; is_aligned pd pd_bits; kheap s (pd + (UCAST(12 \<rightarrow> 32) ad << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (pd + (UCAST(12 \<rightarrow> 32) ad << 2) && mask pd_bits >> 2) := InvalidPDE)))); asid_table s ab = Some bb; asid_table s ac = Some b; b \<noteq> pd + (UCAST(12 \<rightarrow> 32) ad << 2) && ~~ mask pd_bits; kheap s bb = Some (ArchObj (ASIDPool x1)); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ac; be \<noteq> pd + (UCAST(12 \<rightarrow> 32) ad << 2) && ~~ mask pd_bits; kheap s b = Some (ArchObj (ASIDPool x1a)); x1 a = Some pd; ad \<notin> kernel_mapping_slots; pde_ref (x3 ad) = Some pt\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s pda ab bb ac b x1 x1a a ad ae. \<lbrakk>x1a ae = Some (pd + (UCAST(12 \<rightarrow> 32) ad << 2) && ~~ mask pd_bits); UCAST(10 \<rightarrow> 32) ae = UCAST(10 \<rightarrow> 32) a; vaddr >> 20 = UCAST(12 \<rightarrow> 32) ad; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a; UCAST(7 \<rightarrow> 32) ab = UCAST(7 \<rightarrow> 32) ac; is_aligned pd pd_bits; kheap s (pd + (UCAST(12 \<rightarrow> 32) ad << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (pd + (UCAST(12 \<rightarrow> 32) ad << 2) && mask pd_bits >> 2) := InvalidPDE)))); asid_table s ab = Some bb; asid_table s ac = Some b; b \<noteq> pd + (UCAST(12 \<rightarrow> 32) ad << 2) && ~~ mask pd_bits; kheap s bb = Some (ArchObj (ASIDPool x1)); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ac; kheap s b = Some (ArchObj (ASIDPool x1a)); x1 a = Some pd; ad \<notin> kernel_mapping_slots; ad \<noteq> UCAST(32 \<rightarrow> 12) (pd + (UCAST(12 \<rightarrow> 32) ad << 2) && mask pd_bits >> 2); pde_ref (pda ad) = Some pt\<rbrakk> \<Longrightarrow> False
 2. \<And>s pda ab bb ac b x1 x3 x1a a ad ae be. \<lbrakk>x1a ae = Some be; UCAST(10 \<rightarrow> 32) ae = UCAST(10 \<rightarrow> 32) a; vaddr >> 20 = UCAST(12 \<rightarrow> 32) ad; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a; kheap s be = Some (ArchObj (PageDirectory x3)); UCAST(7 \<rightarrow> 32) ab = UCAST(7 \<rightarrow> 32) ac; is_aligned pd pd_bits; kheap s (pd + (UCAST(12 \<rightarrow> 32) ad << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (pd + (UCAST(12 \<rightarrow> 32) ad << 2) && mask pd_bits >> 2) := InvalidPDE)))); asid_table s ab = Some bb; asid_table s ac = Some b; b \<noteq> pd + (UCAST(12 \<rightarrow> 32) ad << 2) && ~~ mask pd_bits; kheap s bb = Some (ArchObj (ASIDPool x1)); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ac; be \<noteq> pd + (UCAST(12 \<rightarrow> 32) ad << 2) && ~~ mask pd_bits; kheap s b = Some (ArchObj (ASIDPool x1a)); x1 a = Some pd; ad \<notin> kernel_mapping_slots; pde_ref (x3 ad) = Some pt\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pda ab bb ac b x1 x3 x1a a ad ae be. \<lbrakk>x1a ae = Some be; UCAST(10 \<rightarrow> 32) ae = UCAST(10 \<rightarrow> 32) a; vaddr >> 20 = UCAST(12 \<rightarrow> 32) ad; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a; kheap s be = Some (ArchObj (PageDirectory x3)); UCAST(7 \<rightarrow> 32) ab = UCAST(7 \<rightarrow> 32) ac; is_aligned pd pd_bits; kheap s pd = Some (ArchObj (PageDirectory pda)); a_type (ArchObj (PageDirectory pda)) = a_type (ArchObj (PageDirectory (pda(ad := InvalidPDE)))); asid_table s ab = Some bb; asid_table s ac = Some b; b \<noteq> pd; kheap s bb = Some (ArchObj (ASIDPool x1)); UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) ac; be \<noteq> pd; kheap s b = Some (ArchObj (ASIDPool x1a)); x1 a = Some pd; ad \<notin> kernel_mapping_slots; pde_ref (x3 ad) = Some pt\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!