theory ArchDomainSepInv

lemma perform_page_table_invocation_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and valid_pti pgi\<rbrace>
   perform_page_table_invocation pgi
   \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" apply (rule hoare_pre) apply (simp add: perform_page_table_invocation_def) apply (wpsimp wp: perform_page_invocation_domain_sep_inv_get_cap_helper
                     crunch_wps set_cap_domain_sep_inv) apply (clarsimp simp: valid_pti_def) apply (case_tac x, simp_all add: domain_sep_inv_cap_def is_pt_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and valid_pti pgi\<rbrace> perform_page_table_invocation pgi \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> perform_page_table_invocation pgi \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>s. (domain_sep_inv irqs st and valid_pti pgi) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case pgi of PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | PageTableUnmap (ArchObjectCap (PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (ArchObjectCap $ update_map_data cap None) ct_slot
od | PageTableUnmap (ArchObjectCap _) ct_slot \<Rightarrow> fail | PageTableUnmap _ ct_slot \<Rightarrow> fail \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>s. (domain_sep_inv irqs st and valid_pti pgi) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (domain_sep_inv irqs st and valid_pti pgi) s \<Longrightarrow> (\<forall>x xa xb xc. pgi = PageTableMap x xa xb xc \<longrightarrow> (domain_sep_inv irqs st and K (domain_sep_inv_cap irqs x)) s) \<and> (\<forall>x xa. pgi = PageTableUnmap x xa \<longrightarrow> (x = NullCap \<longrightarrow> True) \<and> (\<forall>xa xb xc xd. x = UntypedCap xa xb xc xd \<longrightarrow> True) \<and> (\<forall>xa xb xc. x = EndpointCap xa xb xc \<longrightarrow> True) \<and> (\<forall>xa xb xc. x = NotificationCap xa xb xc \<longrightarrow> True) \<and> (\<forall>xa xb xc. x = ReplyCap xa xb xc \<longrightarrow> True) \<and> (\<forall>xa xb xc. x = CNodeCap xa xb xc \<longrightarrow> True) \<and> (\<forall>xa. x = ThreadCap xa \<longrightarrow> True) \<and> (x = DomainCap \<longrightarrow> True) \<and> (x = IRQControlCap \<longrightarrow> True) \<and> (\<forall>xa. x = IRQHandlerCap xa \<longrightarrow> True) \<and> (\<forall>xa xb xc. x = Zombie xa xb xc \<longrightarrow> True) \<and> (\<forall>xa. x = ArchObjectCap xa \<longrightarrow> (\<forall>x xb. xa = ASIDPoolCap x xb \<longrightarrow> True) \<and> (xa = ASIDControlCap \<longrightarrow> True) \<and> (\<forall>x xb xc xd xe. xa = PageCap x xb xc xd xe \<longrightarrow> True) \<and> (\<forall>x xb. xa = PageTableCap x xb \<longrightarrow> (xb = None \<longrightarrow> domain_sep_inv irqs st s) \<and> (\<forall>x. xb = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> domain_sep_inv irqs st s))) \<and> (\<forall>x xb. xa = PageDirectoryCap x xb \<longrightarrow> True))) proof (prove)
goal (1 subgoal):
 1. \<And>s x a b xa xb p' ref y ao. \<lbrakk>domain_sep_inv irqs st s; pgi = PageTableMap x (a, b) xa xb; pde_at xb s; wellformed_pde xa; valid_pde xa s; s \<turnstile> x; cte_wp_at (\<lambda>c. is_arch_update x c \<and> cap_asid c = None) (a, b) s; empty_pde_at xb s; is_pt_cap x; cap_asid x = Some y; vs_cap_ref x = Some (VSRef (xb && mask pd_bits >> 2) (Some APageDirectory) # ref); (ref \<rhd> (xb && ~~ mask pd_bits)) s; pde_ref xa = Some p'; p' \<in> obj_refs x; VSRef (xb && mask pd_bits >> 2) (Some APageDirectory) \<notin> kernel_vsrefs; ako_at ao p' s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> domain_sep_inv_cap irqs x proof (prove)
goal:
No subgoals!