theory PageTableDuplicates

lemma performArchInvocation_valid_duplicates':
  "\<lbrace>invs' and valid_arch_inv' ai and ct_active' and st_tcb_at' active' p
    and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace>
     Arch.performInvocation ai
   \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (simp add: ARM_H.performInvocation_def performARMMMUInvocation_def) apply (cases ai, simp_all) apply (rename_tac page_table_invocation) apply (case_tac page_table_invocation) apply (rule hoare_name_pre_state) apply (clarsimp simp:valid_arch_inv'_def valid_pti'_def isCap_simps
              cte_wp_at_ctes_of is_arch_update'_def isPageTableCap_def
              split:arch_capability.splits) apply (clarsimp simp: performPageTableInvocation_def) apply (rule hoare_pre) apply (simp | wp getSlotCap_inv mapM_x_storePTE_invalid_whole[unfolded swp_def]
           | wpc)+ apply fastforce apply (rule hoare_name_pre_state) apply (clarsimp simp: valid_arch_inv'_def isCap_simps valid_pti'_def
                            cte_wp_at_ctes_of is_arch_update'_def isPageTableCap_def
                      split: arch_capability.splits) apply (clarsimp simp: performPageTableInvocation_def) apply (wp storePDE_no_duplicates' | simp)+ apply (rename_tac page_directory_invocation) apply (case_tac page_directory_invocation,
            simp_all add:performPageDirectoryInvocation_def)[] apply (wp+, simp) apply (wp)+ apply simp apply simp apply(wp, simp) apply (rename_tac asidcontrol_invocation) apply (case_tac asidcontrol_invocation) apply (simp add:performASIDControlInvocation_def ) apply (clarsimp simp:valid_aci'_def valid_arch_inv'_def) apply (rule hoare_name_pre_state) apply (clarsimp simp:cte_wp_at_ctes_of) apply (case_tac ctea,clarsimp) apply (frule(1) ctes_of_valid_cap'[OF _ invs_valid_objs']) apply (wp hoare_weak_lift_imp|simp)+ apply (simp add:placeNewObject_def) apply (wp |simp add:alignError_def unless_def|wpc)+ apply (wp updateFreeIndex_pspace_no_overlap' hoare_drop_imp
        getSlotCap_cte_wp_at deleteObject_no_overlap
        deleteObjects_invs_derivatives[where p="makePoolParent (case ai of InvokeASIDControl i \<Rightarrow> i)"]
        deleteObject_no_overlap
        deleteObjects_cte_wp_at')+ apply (clarsimp simp:cte_wp_at_ctes_of) apply (strengthen refl ctes_of_valid_cap'[mk_strg I E]) apply (clarsimp simp: conj_comms valid_cap_simps' capAligned_def
                         descendants_range'_def2 empty_descendants_range_in') apply (intro conjI; clarsimp) apply (drule(1) cte_cap_in_untyped_range, fastforce simp:cte_wp_at_ctes_of, simp_all)[1] apply (clarsimp simp: invs'_def valid_state'_def if_unsafe_then_cap'_def cte_wp_at_ctes_of) apply clarsimp apply (rename_tac asidpool_invocation) apply (case_tac asidpool_invocation) apply (clarsimp simp:performASIDPoolInvocation_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and valid_arch_inv' ai and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> Arch.performInvocation ai \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and valid_arch_inv' ai and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (case ai of invocation.InvokePageTable oper \<Rightarrow> do performPageTableInvocation oper;
return []
od | invocation.InvokePageDirectory oper \<Rightarrow> do performPageDirectoryInvocation oper;
return []
od | invocation.InvokePage x \<Rightarrow> performPageInvocation x | invocation.InvokeASIDControl oper \<Rightarrow> do performASIDControlInvocation oper;
return []
od | invocation.InvokeASIDPool oper \<Rightarrow> do performASIDPoolInvocation oper;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x1. ai = invocation.InvokePageTable x1 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageTable x1) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageTableInvocation x1;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x2. ai = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageDirectoryInvocation x2;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>page_table_invocation. ai = invocation.InvokePageTable page_table_invocation \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageTable page_table_invocation) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageTableInvocation page_table_invocation;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x2. ai = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageDirectoryInvocation x2;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>page_table_invocation x11 x12. \<lbrakk>ai = invocation.InvokePageTable page_table_invocation; page_table_invocation = ARM_H.PageTableUnmap x11 x12\<rbrakk> \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageTable page_table_invocation) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageTableInvocation page_table_invocation;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>page_table_invocation x21 x22 x23 x24. \<lbrakk>ai = invocation.InvokePageTable page_table_invocation; page_table_invocation = ARM_H.PageTableMap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageTable page_table_invocation) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageTableInvocation page_table_invocation;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x2. ai = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageDirectoryInvocation x2;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>page_table_invocation x11 x12 s. \<lbrakk>ai = invocation.InvokePageTable page_table_invocation; page_table_invocation = ARM_H.PageTableUnmap x11 x12; (invs' and valid_arch_inv' (invocation.InvokePageTable page_table_invocation) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftE (do y <- performPageTableInvocation page_table_invocation;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>page_table_invocation x21 x22 x23 x24. \<lbrakk>ai = invocation.InvokePageTable page_table_invocation; page_table_invocation = ARM_H.PageTableMap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageTable page_table_invocation) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageTableInvocation page_table_invocation;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x2. ai = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageDirectoryInvocation x2;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x12 s cte v0 v1 data. \<lbrakk>ai = invocation.InvokePageTable (ARM_H.PageTableUnmap (arch_capability.PageTableCap v0 v1) x12); invs' s; valid_cap' (capability.ArchObjectCap (arch_capability.PageTableCap v0 v1)) s; ctes_of s x12 = Some cte; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); cteCap cte = capability.ArchObjectCap (arch_capability.PageTableCap v0 data)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftE (do y <- performPageTableInvocation (ARM_H.PageTableUnmap (arch_capability.PageTableCap v0 v1) x12);
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>page_table_invocation x21 x22 x23 x24. \<lbrakk>ai = invocation.InvokePageTable page_table_invocation; page_table_invocation = ARM_H.PageTableMap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageTable page_table_invocation) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageTableInvocation page_table_invocation;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x2. ai = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageDirectoryInvocation x2;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x12 s cte v0 v1 data. \<lbrakk>ai = invocation.InvokePageTable (ARM_H.PageTableUnmap (arch_capability.PageTableCap v0 v1) x12); invs' s; valid_cap' (capability.ArchObjectCap (arch_capability.PageTableCap v0 v1)) s; ctes_of s x12 = Some cte; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); cteCap cte = capability.ArchObjectCap (arch_capability.PageTableCap v0 data)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftE (do y <- do y <- case v1 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do y <- unmapPageTable asid vaddr v0;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [v0 , v0 + 2 ^ pteBits .e. v0 + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU v0 (v0 + 2 ^ ptBits - 1) (addrFromPPtr v0))
od;
cap <- liftM capCap (getSlotCap x12);
updateCap x12 (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>page_table_invocation x21 x22 x23 x24. \<lbrakk>ai = invocation.InvokePageTable page_table_invocation; page_table_invocation = ARM_H.PageTableMap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageTable page_table_invocation) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageTableInvocation page_table_invocation;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x2. ai = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageDirectoryInvocation x2;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x12 s cte v0 v1 data. \<lbrakk>ai = invocation.InvokePageTable (ARM_H.PageTableUnmap (arch_capability.PageTableCap v0 v1) x12); invs' s; valid_cap' (capability.ArchObjectCap (arch_capability.PageTableCap v0 v1)) s; ctes_of s x12 = Some cte; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); cteCap cte = capability.ArchObjectCap (arch_capability.PageTableCap v0 data)\<rbrakk> \<Longrightarrow> \<lbrace>?Q26 x12 s cte v0 v1 data\<rbrace> liftE (do y <- do y <- case v1 of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do y <- unmapPageTable asid vaddr v0;
y <- mapM_x (swp storePTE ARM_H.InvalidPTE) [v0 , v0 + 2 ^ pteBits .e. v0 + 2 ^ ptBits - 1];
doMachineOp (cleanCacheRange_PoU v0 (v0 + 2 ^ ptBits - 1) (addrFromPPtr v0))
od;
cap <- liftM capCap (getSlotCap x12);
updateCap x12 (capability.ArchObjectCap (capPTMappedAddress_update (\<lambda>_. None) cap))
od;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x12 s cte v0 v1 data sa. \<lbrakk>ai = invocation.InvokePageTable (ARM_H.PageTableUnmap (arch_capability.PageTableCap v0 v1) x12); invs' s; valid_cap' (capability.ArchObjectCap (arch_capability.PageTableCap v0 v1)) s; ctes_of s x12 = Some cte; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); cteCap cte = capability.ArchObjectCap (arch_capability.PageTableCap v0 data); s = sa\<rbrakk> \<Longrightarrow> ?Q26 x12 s cte v0 v1 data sa
 3. \<And>page_table_invocation x21 x22 x23 x24. \<lbrakk>ai = invocation.InvokePageTable page_table_invocation; page_table_invocation = ARM_H.PageTableMap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageTable page_table_invocation) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageTableInvocation page_table_invocation;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x2. ai = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageDirectoryInvocation x2;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 7. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x12 s cte v0 v1 data sa. \<lbrakk>ai = invocation.InvokePageTable (ARM_H.PageTableUnmap (arch_capability.PageTableCap v0 v1) x12); invs' sa; valid_cap' (capability.ArchObjectCap (arch_capability.PageTableCap v0 v1)) sa; ctes_of sa x12 = Some cte; ct_active' sa; st_tcb_at' active' p sa; vs_valid_duplicates' (ksPSpace sa); cteCap cte = capability.ArchObjectCap (arch_capability.PageTableCap v0 data); s = sa\<rbrakk> \<Longrightarrow> \<forall>a b. v1 = Some (a, b) \<longrightarrow> valid_cap' (capability.ArchObjectCap (arch_capability.PageTableCap v0 (?option90 x12 sa cte v0 (Some (a, b)) data (a, b) a b))) sa \<and> pspace_aligned' sa
 2. \<And>page_table_invocation x21 x22 x23 x24. \<lbrakk>ai = invocation.InvokePageTable page_table_invocation; page_table_invocation = ARM_H.PageTableMap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageTable page_table_invocation) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageTableInvocation page_table_invocation;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x2. ai = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageDirectoryInvocation x2;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>page_table_invocation x21 x22 x23 x24. \<lbrakk>ai = invocation.InvokePageTable page_table_invocation; page_table_invocation = ARM_H.PageTableMap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageTable page_table_invocation) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageTableInvocation page_table_invocation;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x2. ai = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageDirectoryInvocation x2;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>page_table_invocation x21 x22 x23 x24 s. \<lbrakk>ai = invocation.InvokePageTable page_table_invocation; page_table_invocation = ARM_H.PageTableMap x21 x22 x23 x24; (invs' and valid_arch_inv' (invocation.InvokePageTable page_table_invocation) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftE (do y <- performPageTableInvocation page_table_invocation;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x2. ai = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageDirectoryInvocation x2;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x22 x23 x24 s cte v0. \<lbrakk>ai = invocation.InvokePageTable (ARM_H.PageTableMap (capability.ArchObjectCap v0) x22 x23 x24); invs' s; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) x24 s; ctes_of s x22 = Some cte; valid_cap' (capability.ArchObjectCap v0) s; capMasterCap (capability.ArchObjectCap v0) = capMasterCap (cteCap cte); valid_pde' x23 s; valid_pde_mapping' (x24 && mask pdBits) x23; vs_entry_align (KOArch (KOPDE x23)) = 0; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftE (do y <- performPageTableInvocation (ARM_H.PageTableMap (capability.ArchObjectCap v0) x22 x23 x24);
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x2. ai = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageDirectoryInvocation x2;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x22 x23 x24 s cte v0. \<lbrakk>ai = invocation.InvokePageTable (ARM_H.PageTableMap (capability.ArchObjectCap v0) x22 x23 x24); invs' s; ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) x24 s; ctes_of s x22 = Some cte; valid_cap' (capability.ArchObjectCap v0) s; capMasterCap (capability.ArchObjectCap v0) = capMasterCap (cteCap cte); valid_pde' x23 s; valid_pde_mapping' (x24 && mask pdBits) x23; vs_entry_align (KOArch (KOPDE x23)) = 0; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftE (do y <- do y <- updateCap x22 (capability.ArchObjectCap v0);
y <- storePDE x24 x23;
doMachineOp (cleanByVA_PoU x24 (addrFromPPtr x24))
od;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x2. ai = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performPageDirectoryInvocation x2;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x2. ai = invocation.InvokePageDirectory x2 \<Longrightarrow> \<lbrace>?Q146 x2\<rbrace> performPageDirectoryInvocation x2 \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>x2 s. \<lbrakk>ai = invocation.InvokePageDirectory x2; (invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> ?Q146 x2 s
 3. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>page_directory_invocation. ai = invocation.InvokePageDirectory page_directory_invocation \<Longrightarrow> \<lbrace>?Q146 page_directory_invocation\<rbrace> performPageDirectoryInvocation page_directory_invocation \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>x2 s. \<lbrakk>ai = invocation.InvokePageDirectory x2; (invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> ?Q146 x2 s
 3. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>page_directory_invocation. \<lbrakk>ai = invocation.InvokePageDirectory ARM_H.PageDirectoryNothing; page_directory_invocation = ARM_H.PageDirectoryNothing\<rbrakk> \<Longrightarrow> \<lbrace>?Q146 ARM_H.PageDirectoryNothing\<rbrace> return () \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 2. \<And>page_directory_invocation x21 x22 x23 x24 x25 x26. \<lbrakk>ai = invocation.InvokePageDirectory (ARM_H.PageDirectoryFlush x21 x22 x23 x24 x25 x26); page_directory_invocation = ARM_H.PageDirectoryFlush x21 x22 x23 x24 x25 x26\<rbrakk> \<Longrightarrow> \<lbrace>?Q146 (ARM_H.PageDirectoryFlush x21 x22 x23 x24 x25 x26)\<rbrace> when (x22 < x23) (do root_switched <- setVMRootForFlush x25 x26;
y <- doMachineOp (doFlush x21 x22 x23 x24);
when root_switched (getCurThread >>= setVMRoot)
od) \<lbrace>\<lambda>y a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>x2 s. \<lbrakk>ai = invocation.InvokePageDirectory x2; (invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> ?Q146 x2 s
 4. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>page_directory_invocation x21 x22 x23 x24 x25 x26 root_switched. \<lbrakk>ai = invocation.InvokePageDirectory (ARM_H.PageDirectoryFlush x21 x22 x23 x24 x25 x26); page_directory_invocation = ARM_H.PageDirectoryFlush x21 x22 x23 x24 x25 x26; x22 < x23\<rbrakk> \<Longrightarrow> \<lbrace>?B161 (ARM_H.PageDirectoryFlush x21 x22 x23 x24 x25 x26) x21 x22 x23 x24 x25 x26 root_switched\<rbrace> doMachineOp (doFlush x21 x22 x23 x24) \<lbrace>\<lambda>y s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>page_directory_invocation x21 x22 x23 x24 x25 x26. \<lbrakk>ai = invocation.InvokePageDirectory (ARM_H.PageDirectoryFlush x21 x22 x23 x24 x25 x26); page_directory_invocation = ARM_H.PageDirectoryFlush x21 x22 x23 x24 x25 x26; x22 < x23\<rbrakk> \<Longrightarrow> \<lbrace>?Q160 page_directory_invocation x21 x22 x23 x24 x25 x26\<rbrace> setVMRootForFlush x25 x26 \<lbrace>?B161 page_directory_invocation x21 x22 x23 x24 x25 x26\<rbrace>
 3. \<And>page_directory_invocation x21 x22 x23 x24 x25 x26 s. \<lbrakk>ai = invocation.InvokePageDirectory (ARM_H.PageDirectoryFlush x21 x22 x23 x24 x25 x26); page_directory_invocation = ARM_H.PageDirectoryFlush x21 x22 x23 x24 x25 x26; vs_valid_duplicates' (ksPSpace s)\<rbrakk> \<Longrightarrow> (if x22 < x23 then ?Q160 page_directory_invocation x21 x22 x23 x24 x25 x26 else (\<lambda>a. vs_valid_duplicates' (ksPSpace a))) s
 4. \<And>x2 s. \<lbrakk>ai = invocation.InvokePageDirectory x2; (invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 5. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 7. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>page_directory_invocation x21 x22 x23 x24 x25 x26 s. \<lbrakk>ai = invocation.InvokePageDirectory (ARM_H.PageDirectoryFlush x21 x22 x23 x24 x25 x26); page_directory_invocation = ARM_H.PageDirectoryFlush x21 x22 x23 x24 x25 x26; vs_valid_duplicates' (ksPSpace s)\<rbrakk> \<Longrightarrow> (if x22 < x23 then \<lambda>s. vs_valid_duplicates' (ksPSpace s) else (\<lambda>a. vs_valid_duplicates' (ksPSpace a))) s
 2. \<And>x2 s. \<lbrakk>ai = invocation.InvokePageDirectory x2; (invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 3. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x2 s. \<lbrakk>ai = invocation.InvokePageDirectory x2; (invs' and valid_arch_inv' (invocation.InvokePageDirectory x2) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 2. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x3. ai = invocation.InvokePage x3 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokePage x3) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (performPageInvocation x3) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x4. ai = invocation.InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl x4) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation x4;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>asidcontrol_invocation. ai = invocation.InvokeASIDControl asidcontrol_invocation \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl asidcontrol_invocation) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation asidcontrol_invocation;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>asidcontrol_invocation x1 x2 x3 x4. \<lbrakk>ai = invocation.InvokeASIDControl asidcontrol_invocation; asidcontrol_invocation = asidcontrol_invocation.MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl asidcontrol_invocation) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDControlInvocation asidcontrol_invocation;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>asidcontrol_invocation x1 x2 x3 x4. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); asidcontrol_invocation = asidcontrol_invocation.MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4)) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- do y <- deleteObjects x1 pageBits;
pcap <- getSlotCap x3;
y <- updateFreeIndex x3 (max_free_index (capBlockSize pcap));
y <- placeNewObject x1 makeObject 0;
y <- cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap x1 x4)) x3 x2;
y <- assert (x4 && mask local.asid_low_bits = 0);
asidTable <- gets (armKSASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. asidTable(UCAST(7 \<rightarrow> 32) (asid_high_bits_of x4) \<mapsto> x1)) (ksArchState s)\<rparr>)
od;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4. ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4) \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x2 s \<and> cte_wp_at' (\<lambda>cte. \<exists>idx. cteCap cte = capability.UntypedCap False x1 pageBits idx) x3 s \<and> descendants_of' x3 (ctes_of s) = {} \<and> x2 \<noteq> x3 \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x2 s \<and> sch_act_simple s \<and> is_aligned x4 local.asid_low_bits \<and> x4 < 2 ^ local.asid_bits) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- do y <- deleteObjects x1 pageBits;
pcap <- getSlotCap x3;
y <- updateFreeIndex x3 (max_free_index (capBlockSize pcap));
y <- placeNewObject x1 makeObject 0;
y <- cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap x1 x4)) x3 x2;
y <- assert (x4 && mask local.asid_low_bits = 0);
asidTable <- gets (armKSASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. asidTable(UCAST(7 \<rightarrow> 32) (asid_high_bits_of x4) \<mapsto> x1)) (ksArchState s)\<rparr>)
od;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 s. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); (invs' and (\<lambda>s. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x2 s \<and> cte_wp_at' (\<lambda>cte. \<exists>idx. cteCap cte = capability.UntypedCap False x1 pageBits idx) x3 s \<and> descendants_of' x3 (ctes_of s) = {} \<and> x2 \<noteq> x3 \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x2 s \<and> sch_act_simple s \<and> is_aligned x4 local.asid_low_bits \<and> x4 < 2 ^ local.asid_bits) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftE (do y <- do y <- deleteObjects x1 pageBits;
pcap <- getSlotCap x3;
y <- updateFreeIndex x3 (max_free_index (capBlockSize pcap));
y <- placeNewObject x1 makeObject 0;
y <- cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap x1 x4)) x3 x2;
y <- assert (x4 && mask local.asid_low_bits = 0);
asidTable <- gets (armKSASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. asidTable(UCAST(7 \<rightarrow> 32) (asid_high_bits_of x4) \<mapsto> x1)) (ksArchState s)\<rparr>)
od;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 s cte ctea idx. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some ctea; cteCap ctea = capability.UntypedCap False x1 pageBits idx; x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftE (do y <- do y <- deleteObjects x1 pageBits;
pcap <- getSlotCap x3;
y <- updateFreeIndex x3 (max_free_index (capBlockSize pcap));
y <- placeNewObject x1 makeObject 0;
y <- cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap x1 x4)) x3 x2;
y <- assert (x4 && mask local.asid_low_bits = 0);
asidTable <- gets (armKSASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. asidTable(UCAST(7 \<rightarrow> 32) (asid_high_bits_of x4) \<mapsto> x1)) (ksArchState s)\<rparr>)
od;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 s cte idx x2a. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftE (do y <- do y <- deleteObjects x1 pageBits;
pcap <- getSlotCap x3;
y <- updateFreeIndex x3 (max_free_index (capBlockSize pcap));
y <- placeNewObject x1 makeObject 0;
y <- cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap x1 x4)) x3 x2;
y <- assert (x4 && mask local.asid_low_bits = 0);
asidTable <- gets (armKSASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. asidTable(UCAST(7 \<rightarrow> 32) (asid_high_bits_of x4) \<mapsto> x1)) (ksArchState s)\<rparr>)
od;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 s cte idx x2a. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); valid_cap' (capability.UntypedCap False x1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftE (do y <- do y <- deleteObjects x1 pageBits;
pcap <- getSlotCap x3;
y <- updateFreeIndex x3 (max_free_index (capBlockSize pcap));
y <- placeNewObject x1 makeObject 0;
y <- cteInsert (capability.ArchObjectCap (arch_capability.ASIDPoolCap x1 x4)) x3 x2;
y <- assert (x4 && mask local.asid_low_bits = 0);
asidTable <- gets (armKSASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDTable_update (\<lambda>_. asidTable(UCAST(7 \<rightarrow> 32) (asid_high_bits_of x4) \<mapsto> x1)) (ksArchState s)\<rparr>)
od;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x1 x2 x3 x4 s cte idx x2a pcap. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); valid_cap' (capability.UntypedCap False x1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'237 x1 x2 x3 x4 s cte idx x2a () pcap ()\<rbrace> placeNewObject x1 makeObject 0 \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x1 x2 x3 x4 s cte idx x2a y pcap. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); valid_cap' (capability.UntypedCap False x1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B221 x1 x2 x3 x4 s cte idx x2a y pcap\<rbrace> updateFreeIndex x3 (max_free_index (capBlockSize pcap)) \<lbrace>\<lambda>ya sa. x4 && mask local.asid_low_bits = 0 \<longrightarrow> ?P'237 x1 x2 x3 x4 s cte idx x2a y pcap ya sa\<rbrace>
 3. \<And>x1 x2 x3 x4 s cte idx x2a y. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); valid_cap' (capability.UntypedCap False x1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B220 x1 x2 x3 x4 s cte idx x2a y\<rbrace> getSlotCap x3 \<lbrace>?B221 x1 x2 x3 x4 s cte idx x2a y\<rbrace>
 4. \<And>x1 x2 x3 x4 s cte idx x2a. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); valid_cap' (capability.UntypedCap False x1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q215 x1 x2 x3 x4 s cte idx x2a\<rbrace> deleteObjects x1 pageBits \<lbrace>?B220 x1 x2 x3 x4 s cte idx x2a\<rbrace>
 5. \<And>x1 x2 x3 x4 s cte idx x2a sa. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); valid_cap' (capability.UntypedCap False x1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> ?Q215 x1 x2 x3 x4 s cte idx x2a sa
 6. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x1 x2 x3 x4 s cte idx x2a pcap. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); valid_cap' (capability.UntypedCap False x1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?P'237 x1 x2 x3 x4 s cte idx x2a () pcap ()\<rbrace> placeNewObject' x1 (KOArch (KOASIDPool makeObject)) 0 \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>x1 x2 x3 x4 s cte idx x2a y pcap. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); valid_cap' (capability.UntypedCap False x1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B221 x1 x2 x3 x4 s cte idx x2a y pcap\<rbrace> updateFreeIndex x3 (max_free_index (capBlockSize pcap)) \<lbrace>\<lambda>ya sa. x4 && mask local.asid_low_bits = 0 \<longrightarrow> ?P'237 x1 x2 x3 x4 s cte idx x2a y pcap ya sa\<rbrace>
 3. \<And>x1 x2 x3 x4 s cte idx x2a y. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); valid_cap' (capability.UntypedCap False x1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B220 x1 x2 x3 x4 s cte idx x2a y\<rbrace> getSlotCap x3 \<lbrace>?B221 x1 x2 x3 x4 s cte idx x2a y\<rbrace>
 4. \<And>x1 x2 x3 x4 s cte idx x2a. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); valid_cap' (capability.UntypedCap False x1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q215 x1 x2 x3 x4 s cte idx x2a\<rbrace> deleteObjects x1 pageBits \<lbrace>?B220 x1 x2 x3 x4 s cte idx x2a\<rbrace>
 5. \<And>x1 x2 x3 x4 s cte idx x2a sa. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); valid_cap' (capability.UntypedCap False x1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> ?Q215 x1 x2 x3 x4 s cte idx x2a sa
 6. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2 x3 x4 s cte idx x2a pcap. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); valid_cap' (capability.UntypedCap False x1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B221 x1 x2 x3 x4 s cte idx x2a () pcap\<rbrace> updateFreeIndex x3 (max_free_index (capBlockSize pcap)) \<lbrace>\<lambda>ya s. x4 && mask local.asid_low_bits = 0 \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> pspace_no_overlap' x1 pageBits s \<and> is_aligned x1 pageBits \<and> pspace_aligned' s\<rbrace>
 2. \<And>x1 x2 x3 x4 s cte idx x2a y. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); valid_cap' (capability.UntypedCap False x1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?B220 x1 x2 x3 x4 s cte idx x2a y\<rbrace> getSlotCap x3 \<lbrace>?B221 x1 x2 x3 x4 s cte idx x2a y\<rbrace>
 3. \<And>x1 x2 x3 x4 s cte idx x2a. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); valid_cap' (capability.UntypedCap False x1 pageBits idx) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q215 x1 x2 x3 x4 s cte idx x2a\<rbrace> deleteObjects x1 pageBits \<lbrace>?B220 x1 x2 x3 x4 s cte idx x2a\<rbrace>
 4. \<And>x1 x2 x3 x4 s cte idx x2a sa. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); valid_cap' (capability.UntypedCap False x1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> ?Q215 x1 x2 x3 x4 s cte idx x2a sa
 5. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 s cte idx x2a sa. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' s; ctes_of s x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of s) = {}; ctes_of s x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 s; sch_act_simple s; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' s; st_tcb_at' active' p s; vs_valid_duplicates' (ksPSpace s); valid_cap' (capability.UntypedCap False x1 pageBits idx) s; s = sa\<rbrakk> \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and K (is_aligned x1 pageBits)) sa \<and> (valid_cap' (capability.UntypedCap (?d266 x1 x2 x3 x4 s cte idx x2a) x1 pageBits (?idx266 x1 x2 x3 x4 s cte idx x2a)) and valid_pspace') sa \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d269 x1 x2 x3 x4 s cte idx x2a) x1 pageBits (?idx269 x1 x2 x3 x4 s cte idx x2a)) (makePoolParent (case ai of invocation.InvokeASIDControl i \<Rightarrow> i)) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d269 x1 x2 x3 x4 s cte idx x2a) x1 pageBits (?idx269 x1 x2 x3 x4 s cte idx x2a)) (makePoolParent (case ai of invocation.InvokeASIDControl i \<Rightarrow> i)) (ctes_of sa)) and K (pageBits < word_bits \<and> is_aligned x1 pageBits)) sa \<and> (cte_wp_at' (isUntypedCap \<circ> cteCap) x3 sa \<and> x3 \<notin> {x1..x1 + 2 ^ pageBits - 1} \<and> valid_cap' (capability.UntypedCap (?d271 x1 x2 x3 x4 s cte idx x2a) x1 pageBits (?idx271 x1 x2 x3 x4 s cte idx x2a)) sa \<and> valid_pspace' sa) \<and> is_aligned x1 pageBits \<and> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d274 x1 x2 x3 x4 s cte idx x2a) x1 pageBits (?idx274 x1 x2 x3 x4 s cte idx x2a)) (makePoolParent (case ai of invocation.InvokeASIDControl i \<Rightarrow> i)) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d274 x1 x2 x3 x4 s cte idx x2a) x1 pageBits (?idx274 x1 x2 x3 x4 s cte idx x2a)) (makePoolParent (case ai of invocation.InvokeASIDControl i \<Rightarrow> i)) (ctes_of sa)) and K (pageBits < word_bits \<and> is_aligned x1 pageBits)) sa
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 cte idx x2a sa. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' sa; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' sa; st_tcb_at' active' p sa; vs_valid_duplicates' (ksPSpace sa); valid_cap' (capability.UntypedCap False x1 pageBits idx) sa\<rbrakk> \<Longrightarrow> is_aligned x1 pageBits \<and> valid_cap' (capability.UntypedCap (?d266 x1 x2 x3 x4 sa cte idx x2a) x1 pageBits (?idx266 x1 x2 x3 x4 sa cte idx x2a)) sa \<and> valid_pspace' sa \<and> \<not> ?d269 x1 x2 x3 x4 sa cte idx x2a \<and> idx = ?idx269 x1 x2 x3 x4 sa cte idx x2a \<and> descendants_range' (capability.UntypedCap (?d269 x1 x2 x3 x4 sa cte idx x2a) x1 pageBits (?idx269 x1 x2 x3 x4 sa cte idx x2a)) x3 (ctes_of sa) \<and> is_aligned x1 pageBits \<and> (x1 \<le> x3 \<longrightarrow> \<not> x3 \<le> x1 + 2 ^ pageBits - 1) \<and> valid_cap' (capability.UntypedCap (?d271 x1 x2 x3 x4 sa cte idx x2a) x1 pageBits (?idx271 x1 x2 x3 x4 sa cte idx x2a)) sa \<and> valid_pspace' sa \<and> is_aligned x1 pageBits \<and> \<not> ?d274 x1 x2 x3 x4 sa cte idx x2a \<and> idx = ?idx274 x1 x2 x3 x4 sa cte idx x2a \<and> descendants_range' (capability.UntypedCap (?d274 x1 x2 x3 x4 sa cte idx x2a) x1 pageBits (?idx274 x1 x2 x3 x4 sa cte idx x2a)) x3 (ctes_of sa) \<and> is_aligned x1 pageBits
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 cte idx x2a sa. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' sa; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' sa; st_tcb_at' active' p sa; vs_valid_duplicates' (ksPSpace sa); valid_cap' (capability.UntypedCap False x1 pageBits idx) sa\<rbrakk> \<Longrightarrow> is_aligned x1 pageBits \<and> valid_objs' sa \<and> valid_pspace' sa \<and> \<not> \<not> True \<and> True \<and> descendants_range' (capability.UntypedCap (?t294 x1 x2 x3 x4 cte idx x2a sa \<noteq> ?t294 x1 x2 x3 x4 cte idx x2a sa) x1 pageBits idx) x3 (ctes_of sa) \<and> is_aligned x1 pageBits \<and> (x1 \<le> x3 \<longrightarrow> \<not> x3 \<le> x1 + 2 ^ pageBits - 1) \<and> valid_objs' sa \<and> valid_pspace' sa \<and> is_aligned x1 pageBits \<and> \<not> \<not> True \<and> True \<and> descendants_range' (capability.UntypedCap (?t314 x1 x2 x3 x4 cte idx x2a sa \<noteq> ?t314 x1 x2 x3 x4 cte idx x2a sa) x1 pageBits idx) x3 (ctes_of sa) \<and> is_aligned x1 pageBits
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 cte idx x2a sa. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' sa; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' sa; st_tcb_at' active' p sa; vs_valid_duplicates' (ksPSpace sa); is_aligned x1 pageBits; minUntypedSizeBits \<le> pageBits; pageBits \<le> maxUntypedSizeBits; is_aligned (word_of_nat idx) minUntypedSizeBits; x1 \<noteq> 0; valid_untyped' False x1 pageBits idx sa; idx \<le> 2 ^ pageBits\<rbrakk> \<Longrightarrow> valid_objs' sa \<and> valid_pspace' sa \<and> (x1 \<le> x3 \<longrightarrow> \<not> x3 \<le> x1 + 2 ^ pageBits - 1)
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 cte idx x2a sa. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' sa; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' sa; st_tcb_at' active' p sa; vs_valid_duplicates' (ksPSpace sa); is_aligned x1 pageBits; minUntypedSizeBits \<le> pageBits; pageBits \<le> maxUntypedSizeBits; is_aligned (word_of_nat idx) minUntypedSizeBits; x1 \<noteq> 0; valid_untyped' False x1 pageBits idx sa; idx \<le> 2 ^ pageBits; x1 \<le> x3; x3 \<le> x1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> False
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2 x3 x4 cte idx x2a sa. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' sa; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' sa; st_tcb_at' active' p sa; vs_valid_duplicates' (ksPSpace sa); is_aligned x1 pageBits; minUntypedSizeBits \<le> pageBits; pageBits \<le> maxUntypedSizeBits; is_aligned (word_of_nat idx) minUntypedSizeBits; x1 \<noteq> 0; valid_untyped' False x1 pageBits idx sa; idx \<le> 2 ^ pageBits; x3 \<le> x1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) x3 sa
 2. \<And>x1 x2 x3 x4 cte idx x2a sa. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' sa; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' sa; st_tcb_at' active' p sa; vs_valid_duplicates' (ksPSpace sa); is_aligned x1 pageBits; minUntypedSizeBits \<le> pageBits; pageBits \<le> maxUntypedSizeBits; is_aligned (word_of_nat idx) minUntypedSizeBits; x1 \<noteq> 0; valid_untyped' False x1 pageBits idx sa; idx \<le> 2 ^ pageBits; x3 \<le> x1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> valid_global_refs' sa
 3. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 cte idx x2a sa. \<lbrakk>ai = invocation.InvokeASIDControl (asidcontrol_invocation.MakePool x1 x2 x3 x4); invs' sa; ctes_of sa x2 = Some cte; cteCap cte = capability.NullCap; descendants_of' x3 (ctes_of sa) = {}; ctes_of sa x3 = Some (CTE (capability.UntypedCap False x1 pageBits idx) x2a); x2 \<noteq> x3; ex_cte_cap_wp_to' (\<lambda>_. True) x2 sa; sch_act_simple sa; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; ct_active' sa; st_tcb_at' active' p sa; vs_valid_duplicates' (ksPSpace sa); is_aligned x1 pageBits; minUntypedSizeBits \<le> pageBits; pageBits \<le> maxUntypedSizeBits; is_aligned (word_of_nat idx) minUntypedSizeBits; x1 \<noteq> 0; valid_untyped' False x1 pageBits idx sa; idx \<le> 2 ^ pageBits; x3 \<le> x1 + 2 ^ pageBits - 1\<rbrakk> \<Longrightarrow> valid_global_refs' sa
 2. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x5. ai = invocation.InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool x5) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation x5;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>asidpool_invocation. ai = invocation.InvokeASIDPool asidpool_invocation \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool asidpool_invocation) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation asidpool_invocation;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>asidpool_invocation x1 x2 x3. \<lbrakk>ai = invocation.InvokeASIDPool asidpool_invocation; asidpool_invocation = asidpool_invocation.Assign x1 x2 x3\<rbrakk> \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool asidpool_invocation) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- performASIDPoolInvocation asidpool_invocation;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3. ai = invocation.InvokeASIDPool (asidpool_invocation.Assign x1 x2 x3) \<Longrightarrow> \<lbrace>invs' and valid_arch_inv' (invocation.InvokeASIDPool (asidpool_invocation.Assign x1 x2 x3)) and ct_active' and st_tcb_at' active' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> liftE (do y <- do oldcap <- getSlotCap x3;
pool <- liftM (inv asidpool.ASIDPool) (getObject x2);
y <- updateCap x3 (capability.ArchObjectCap (capPDMappedASID_update (\<lambda>_. Some x1) (capCap oldcap)));
setObject x2 (asidpool.ASIDPool (pool(x1 && mask local.asid_low_bits \<mapsto> capPDBasePtr (capCap oldcap))))
od;
return []
od) \<lbrace>\<lambda>reply s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal:
No subgoals!