theory VSpace_R

lemma perform_aci_invs [wp]:
  "\<lbrace>invs' and valid_apinv' api\<rbrace> performASIDPoolInvocation api \<lbrace>\<lambda>_. invs'\<rbrace>" apply (clarsimp simp: performASIDPoolInvocation_def split: asidpool_invocation.splits) apply (wp arch_update_updateCap_invs getASID_wp getSlotCap_wp) apply (clarsimp simp: valid_apinv'_def cte_wp_at_ctes_of) apply (case_tac cte) apply clarsimp apply (drule ctes_of_valid_cap', fastforce) apply (clarsimp simp: isPDCap_def valid_cap'_def capAligned_def is_arch_update'_def isCap_simps) apply (drule ko_at_valid_objs', fastforce, simp add: projectKOs) apply (clarsimp simp: valid_obj'_def ran_def mask_asid_low_bits_ucast_ucast
                 split: if_split_asm) apply (case_tac ko, clarsimp simp: inv_def) apply (clarsimp simp: page_directory_at'_def, drule_tac x=0 in spec) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and valid_apinv' api\<rbrace> performASIDPoolInvocation api \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3. api = asidpool_invocation.Assign x1 x2 x3 \<Longrightarrow> \<lbrace>invs' and valid_apinv' (asidpool_invocation.Assign x1 x2 x3)\<rbrace> 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 \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 s. \<lbrakk>api = asidpool_invocation.Assign x1 x2 x3; (invs' and valid_apinv' (asidpool_invocation.Assign x1 x2 x3)) s\<rbrakk> \<Longrightarrow> \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) x3 s \<and> (\<forall>ko. ko_at' ko x2 s \<longrightarrow> ((\<lambda>pool s. cte_wp_at' (is_arch_update' (capability.ArchObjectCap (capPDMappedASID_update (\<lambda>_. Some x1) (capCap cap)))) x3 s \<and> invs' s \<and> valid_cap' (capability.ArchObjectCap (capPDMappedASID_update (\<lambda>_. Some x1) (capCap cap))) s \<and> valid_asid_pool' (asidpool.ASIDPool (pool(x1 && mask local.asid_low_bits \<mapsto> capPDBasePtr (capCap cap)))) s) \<circ> inv asidpool.ASIDPool) ko s) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 s cte ko. \<lbrakk>api = asidpool_invocation.Assign x1 x2 x3; invs' s; asid_pool_at' x2 s; 0 < x1; x1 < 2 ^ local.asid_bits; ctes_of s x3 = Some cte; isPDCap (cteCap cte); ko_at' ko x2 s\<rbrakk> \<Longrightarrow> is_arch_update' (capability.ArchObjectCap (capPDMappedASID_update (\<lambda>_. Some x1) (capCap (cteCap cte)))) cte \<and> valid_cap' (capability.ArchObjectCap (capPDMappedASID_update (\<lambda>_. Some x1) (capCap (cteCap cte)))) s \<and> x1 && mask local.asid_low_bits \<le> 2 ^ local.asid_low_bits - 1 \<and> dom (inv asidpool.ASIDPool ko) \<subseteq> {0..2 ^ local.asid_low_bits - 1} \<and> 0 \<notin> ran ((inv asidpool.ASIDPool ko)(x1 && mask local.asid_low_bits \<mapsto> capPDBasePtr (capCap (cteCap cte)))) \<and> (\<forall>x\<in>ran ((inv asidpool.ASIDPool ko)(x1 && mask local.asid_low_bits \<mapsto> capPDBasePtr (capCap (cteCap cte)))). is_aligned x pdBits) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 s cte ko x1a x2a. \<lbrakk>api = asidpool_invocation.Assign x1 x2 x3; invs' s; asid_pool_at' x2 s; 0 < x1; x1 < 2 ^ local.asid_bits; ctes_of s x3 = Some cte; isPDCap (cteCap cte); ko_at' ko x2 s; cte = CTE x1a x2a\<rbrakk> \<Longrightarrow> is_arch_update' (capability.ArchObjectCap (capPDMappedASID_update (\<lambda>_. Some x1) (capCap (cteCap cte)))) cte \<and> valid_cap' (capability.ArchObjectCap (capPDMappedASID_update (\<lambda>_. Some x1) (capCap (cteCap cte)))) s \<and> x1 && mask local.asid_low_bits \<le> 2 ^ local.asid_low_bits - 1 \<and> dom (inv asidpool.ASIDPool ko) \<subseteq> {0..2 ^ local.asid_low_bits - 1} \<and> 0 \<notin> ran ((inv asidpool.ASIDPool ko)(x1 && mask local.asid_low_bits \<mapsto> capPDBasePtr (capCap (cteCap cte)))) \<and> (\<forall>x\<in>ran ((inv asidpool.ASIDPool ko)(x1 && mask local.asid_low_bits \<mapsto> capPDBasePtr (capCap (cteCap cte)))). is_aligned x pdBits) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 s ko x1a x2a. \<lbrakk>api = asidpool_invocation.Assign x1 x2 x3; invs' s; asid_pool_at' x2 s; 0 < x1; x1 < 2 ^ local.asid_bits; ctes_of s x3 = Some (CTE x1a x2a); isPDCap x1a; ko_at' ko x2 s\<rbrakk> \<Longrightarrow> is_arch_update' (capability.ArchObjectCap (capPDMappedASID_update (\<lambda>_. Some x1) (capCap x1a))) (CTE x1a x2a) \<and> valid_cap' (capability.ArchObjectCap (capPDMappedASID_update (\<lambda>_. Some x1) (capCap x1a))) s \<and> x1 && mask local.asid_low_bits \<le> 2 ^ local.asid_low_bits - 1 \<and> dom (inv asidpool.ASIDPool ko) \<subseteq> {0..2 ^ local.asid_low_bits - 1} \<and> 0 \<notin> ran ((inv asidpool.ASIDPool ko)(x1 && mask local.asid_low_bits \<mapsto> capPDBasePtr (capCap x1a))) \<and> (\<forall>x\<in>ran ((inv asidpool.ASIDPool ko)(x1 && mask local.asid_low_bits \<mapsto> capPDBasePtr (capCap x1a))). is_aligned x pdBits) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 s ko x1a x2a. \<lbrakk>api = asidpool_invocation.Assign x1 x2 x3; invs' s; asid_pool_at' x2 s; 0 < x1; x1 < 2 ^ local.asid_bits; isPDCap x1a; ko_at' ko x2 s; valid_cap' x1a s\<rbrakk> \<Longrightarrow> is_arch_update' (capability.ArchObjectCap (capPDMappedASID_update (\<lambda>_. Some x1) (capCap x1a))) (CTE x1a x2a) \<and> valid_cap' (capability.ArchObjectCap (capPDMappedASID_update (\<lambda>_. Some x1) (capCap x1a))) s \<and> x1 && mask local.asid_low_bits \<le> 2 ^ local.asid_low_bits - 1 \<and> dom (inv asidpool.ASIDPool ko) \<subseteq> {0..2 ^ local.asid_low_bits - 1} \<and> 0 \<notin> ran ((inv asidpool.ASIDPool ko)(x1 && mask local.asid_low_bits \<mapsto> capPDBasePtr (capCap x1a))) \<and> (\<forall>x\<in>ran ((inv asidpool.ASIDPool ko)(x1 && mask local.asid_low_bits \<mapsto> capPDBasePtr (capCap x1a))). is_aligned x pdBits) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 s ko p asid. \<lbrakk>api = asidpool_invocation.Assign x1 x2 x3; invs' s; asid_pool_at' x2 s; 0 < x1; x1 < 2 ^ local.asid_bits; ko_at' ko x2 s; is_aligned p 14; 14 < word_bits; page_directory_at' p s; case asid of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits\<rbrakk> \<Longrightarrow> x1 && mask local.asid_low_bits \<le> 2 ^ local.asid_low_bits - 1 \<and> dom (inv asidpool.ASIDPool ko) \<subseteq> {0..2 ^ local.asid_low_bits - 1} \<and> 0 \<notin> ran ((inv asidpool.ASIDPool ko)(x1 && mask local.asid_low_bits \<mapsto> p)) \<and> (\<forall>x\<in>ran ((inv asidpool.ASIDPool ko)(x1 && mask local.asid_low_bits \<mapsto> p)). is_aligned x pdBits) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 s ko p asid. \<lbrakk>api = asidpool_invocation.Assign x1 x2 x3; invs' s; asid_pool_at' x2 s; 0 < x1; x1 < 2 ^ local.asid_bits; is_aligned p 14; 14 < word_bits; page_directory_at' p s; case asid of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits; valid_obj' (injectKO ko) s\<rbrakk> \<Longrightarrow> x1 && mask local.asid_low_bits \<le> 2 ^ local.asid_low_bits - 1 \<and> dom (inv asidpool.ASIDPool ko) \<subseteq> {0..2 ^ local.asid_low_bits - 1} \<and> 0 \<notin> ran ((inv asidpool.ASIDPool ko)(x1 && mask local.asid_low_bits \<mapsto> p)) \<and> (\<forall>x\<in>ran ((inv asidpool.ASIDPool ko)(x1 && mask local.asid_low_bits \<mapsto> p)). is_aligned x pdBits) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 s ko p asid. \<lbrakk>api = asidpool_invocation.Assign x1 x2 x3; invs' s; asid_pool_at' x2 s; 0 < x1; x1 < 2 ^ local.asid_bits; is_aligned p 14; 14 < word_bits; page_directory_at' p s; case asid of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits; valid_asid_pool' ko s\<rbrakk> \<Longrightarrow> dom (inv asidpool.ASIDPool ko) \<subseteq> {0..2 ^ local.asid_low_bits - 1} \<and> (\<forall>a. (a = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) \<longrightarrow> p \<noteq> 0) \<and> (a \<noteq> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) \<longrightarrow> inv asidpool.ASIDPool ko a \<noteq> Some 0)) \<and> (\<forall>x. (\<exists>a. (a = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) \<longrightarrow> p = x) \<and> (a \<noteq> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) \<longrightarrow> inv asidpool.ASIDPool ko a = Some x)) \<longrightarrow> is_aligned x pdBits) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 s p asid x. \<lbrakk>api = asidpool_invocation.Assign x1 x2 x3; invs' s; asid_pool_at' x2 s; 0 < x1; x1 < 2 ^ local.asid_bits; is_aligned p 14; 14 < word_bits; page_directory_at' p s; case asid of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits; dom x \<subseteq> {0..2 ^ local.asid_low_bits - 1}; 0 \<notin> ran x; \<forall>x\<in>ran x. is_aligned x pdBits\<rbrakk> \<Longrightarrow> (\<forall>a. (a = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) \<longrightarrow> p \<noteq> 0) \<and> (a \<noteq> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) \<longrightarrow> x a \<noteq> Some 0)) \<and> (\<forall>xa. (\<exists>a. (a = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) \<longrightarrow> p = xa) \<and> (a \<noteq> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) \<longrightarrow> x a = Some xa)) \<longrightarrow> is_aligned xa pdBits) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 s p asid x. \<lbrakk>api = asidpool_invocation.Assign x1 x2 x3; invs' s; asid_pool_at' x2 s; 0 < x1; x1 < 2 ^ local.asid_bits; is_aligned p 14; 14 < word_bits; case asid of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits; dom x \<subseteq> {0..2 ^ local.asid_low_bits - 1}; 0 \<notin> ran x; \<forall>x\<in>ran x. is_aligned x pdBits; is_aligned p pdBits; 0 < 0x1000 \<longrightarrow> pde_at' (p + (0 << 2)) s\<rbrakk> \<Longrightarrow> (\<forall>a. (a = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) \<longrightarrow> p \<noteq> 0) \<and> (a \<noteq> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) \<longrightarrow> x a \<noteq> Some 0)) \<and> (\<forall>xa. (\<exists>a. (a = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) \<longrightarrow> p = xa) \<and> (a \<noteq> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x1) \<longrightarrow> x a = Some xa)) \<longrightarrow> is_aligned xa pdBits) proof (prove)
goal:
No subgoals!