theory VSpace_R

lemma perform_pti_invs [wp]:
  "\<lbrace>invs' and valid_pti' pti\<rbrace> performPageTableInvocation pti \<lbrace>\<lambda>_. invs'\<rbrace>" apply (clarsimp simp: performPageTableInvocation_def getSlotCap_def
                 split: page_table_invocation.splits) apply (intro conjI allI impI) apply (rule hoare_pre) apply (wp arch_update_updateCap_invs getCTE_wp
              hoare_vcg_ex_lift no_irq_cleanCacheRange_PoU mapM_x_wp'
                | wpc | simp add: o_def
                | (simp only: imp_conv_disj, rule hoare_vcg_disj_lift))+ apply (clarsimp simp: valid_pti'_def cte_wp_at_ctes_of
                         is_arch_update'_def isCap_simps valid_cap'_def
                         capAligned_def) apply (rule hoare_pre) apply (wp arch_update_updateCap_invs valid_pde_lift'
             no_irq_cleanByVA_PoU
          | simp)+ apply (clarsimp simp: cte_wp_at_ctes_of valid_pti'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and valid_pti' pti\<rbrace> performPageTableInvocation pti \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<forall>x11 x12. pti = ARM_H.PageTableUnmap x11 x12 \<longrightarrow> \<lbrace>invs' and valid_pti' (ARM_H.PageTableUnmap x11 x12)\<rbrace> do y <- case capPTMappedAddress x11 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do y <- unmapPageTable asid vaddr (capPTBasePtr x11);
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [capPTBasePtr x11 , capPTBasePtr x11 + 2 ^ pteBits .e. capPTBasePtr x11 + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU (capPTBasePtr x11) (capPTBasePtr x11 + 2 ^ ptBits - 1) (addrFromPPtr (capPTBasePtr x11)))
od;
cap <- liftM capCap (do cte <- getCTE x12;
return (cteCap cte)
od);
updateCap x12 (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od \<lbrace>\<lambda>_. invs'\<rbrace>) \<and> (\<forall>x21 x22 x23 x24. pti = ARM_H.PageTableMap x21 x22 x23 x24 \<longrightarrow> \<lbrace>invs' and valid_pti' (ARM_H.PageTableMap x21 x22 x23 x24)\<rbrace> do y <- updateCap x22 x21;
y <- storePDE x24 x23;
doMachineOp (cleanByVA_PoU x24 (addrFromPPtr x24))
od \<lbrace>\<lambda>_. invs'\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12. pti = ARM_H.PageTableUnmap x11 x12 \<Longrightarrow> \<lbrace>invs' and valid_pti' (ARM_H.PageTableUnmap x11 x12)\<rbrace> do y <- case capPTMappedAddress x11 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do y <- unmapPageTable asid vaddr (capPTBasePtr x11);
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [capPTBasePtr x11 , capPTBasePtr x11 + 2 ^ pteBits .e. capPTBasePtr x11 + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU (capPTBasePtr x11) (capPTBasePtr x11 + 2 ^ ptBits - 1) (addrFromPPtr (capPTBasePtr x11)))
od;
cap <- liftM capCap (do cte <- getCTE x12;
return (cteCap cte)
od);
updateCap x12 (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od \<lbrace>\<lambda>_. invs'\<rbrace>
 2. \<And>x21 x22 x23 x24. pti = ARM_H.PageTableMap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>invs' and valid_pti' (ARM_H.PageTableMap x21 x22 x23 x24)\<rbrace> do y <- updateCap x22 x21;
y <- storePDE x24 x23;
doMachineOp (cleanByVA_PoU x24 (addrFromPPtr x24))
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x11 x12. pti = ARM_H.PageTableUnmap x11 x12 \<Longrightarrow> \<lbrace>?Q15 x11 x12\<rbrace> do y <- case capPTMappedAddress x11 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do y <- unmapPageTable asid vaddr (capPTBasePtr x11);
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [capPTBasePtr x11 , capPTBasePtr x11 + 2 ^ pteBits .e. capPTBasePtr x11 + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU (capPTBasePtr x11) (capPTBasePtr x11 + 2 ^ ptBits - 1) (addrFromPPtr (capPTBasePtr x11)))
od;
cap <- liftM capCap (do cte <- getCTE x12;
return (cteCap cte)
od);
updateCap x12 (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od \<lbrace>\<lambda>_. invs'\<rbrace>
 2. \<And>x11 x12 s. \<lbrakk>pti = ARM_H.PageTableUnmap x11 x12; (invs' and valid_pti' (ARM_H.PageTableUnmap x11 x12)) s\<rbrakk> \<Longrightarrow> ?Q15 x11 x12 s
 3. \<And>x21 x22 x23 x24. pti = ARM_H.PageTableMap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>invs' and valid_pti' (ARM_H.PageTableMap x21 x22 x23 x24)\<rbrace> do y <- updateCap x22 x21;
y <- storePDE x24 x23;
doMachineOp (cleanByVA_PoU x24 (addrFromPPtr x24))
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 s. \<lbrakk>pti = ARM_H.PageTableUnmap x11 x12; invs' s \<and> valid_pti' (ARM_H.PageTableUnmap x11 x12) s\<rbrakk> \<Longrightarrow> (capPTMappedAddress x11 = None \<longrightarrow> cte_wp_at' (\<lambda>_. True) x12 s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) x12 s \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) (capCap (cteCap cte))))) x12 s \<and> valid_cap' (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) (capCap (cteCap cte)))) s)) \<and> ((\<exists>a b. capPTMappedAddress x11 = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>a. True) x12 s \<longrightarrow> (\<exists>x. cte_wp_at' ((=) x) x12 s \<and> cte_wp_at' (is_arch_update' (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) (capCap (cteCap x))))) x12 s \<and> valid_cap' (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) (capCap (cteCap x)))) s))
 2. \<And>x21 x22 x23 x24. pti = ARM_H.PageTableMap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>invs' and valid_pti' (ARM_H.PageTableMap x21 x22 x23 x24)\<rbrace> do y <- updateCap x22 x21;
y <- storePDE x24 x23;
doMachineOp (cleanByVA_PoU x24 (addrFromPPtr x24))
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24. pti = ARM_H.PageTableMap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>invs' and valid_pti' (ARM_H.PageTableMap x21 x22 x23 x24)\<rbrace> do y <- updateCap x22 x21;
y <- storePDE x24 x23;
doMachineOp (cleanByVA_PoU x24 (addrFromPPtr x24))
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24. pti = ARM_H.PageTableMap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>?Q179 x21 x22 x23 x24\<rbrace> do y <- updateCap x22 x21;
y <- storePDE x24 x23;
doMachineOp (cleanByVA_PoU x24 (addrFromPPtr x24))
od \<lbrace>\<lambda>_. invs'\<rbrace>
 2. \<And>x21 x22 x23 x24 s. \<lbrakk>pti = ARM_H.PageTableMap x21 x22 x23 x24; (invs' and valid_pti' (ARM_H.PageTableMap x21 x22 x23 x24)) s\<rbrakk> \<Longrightarrow> ?Q179 x21 x22 x23 x24 s proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 s. \<lbrakk>pti = ARM_H.PageTableMap x21 x22 x23 x24; invs' s \<and> valid_pti' (ARM_H.PageTableMap x21 x22 x23 x24) s\<rbrakk> \<Longrightarrow> cte_wp_at' (is_arch_update' x21) x22 s \<and> valid_cap' x21 s \<and> valid_pde' x23 s \<and> valid_pde_mapping' (x24 && mask pdBits) x23 proof (prove)
goal:
No subgoals!