theory ArchVSpace_AI

lemma find_pd_for_asid_aligned_pd [wp]:
  "\<lbrace>pspace_aligned and valid_vspace_objs\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv s. is_aligned rv 14\<rbrace>,-" apply (simp add: find_pd_for_asid_def assertE_def split del: if_split) apply (rule hoare_pre) apply (wp|wpc)+ apply clarsimp apply (drule vs_lookup_atI) apply (drule (2) valid_vspace_objsD) apply clarsimp apply (drule bspec, blast) apply (thin_tac "ko_at ko p s" for ko p) apply (clarsimp simp: pspace_aligned_def obj_at_def) apply (drule bspec, blast) apply (clarsimp simp: a_type_def
                  split: Structures_A.kernel_object.splits arch_kernel_obj.splits if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv s. is_aligned rv 14\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs\<rbrace> doE y <- if 0 < asid then returnOk () else fail;
asid_table <- liftE (gets (arm_asid_table \<circ> arch_state));
pool <- case asid_table (asid_high_bits_of asid) of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE $ get_asid_pool ptr;
case pool (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE \<lbrace>\<lambda>rv s. is_aligned rv 14\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> doE y <- if 0 < asid then returnOk () else fail;
asid_table <- liftE (gets (arm_asid_table \<circ> arch_state));
pool <- case asid_table (asid_high_bits_of asid) of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE $ get_asid_pool ptr;
case pool (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE \<lbrace>\<lambda>rv s. is_aligned rv 14\<rbrace>, -
 2. \<And>s. (pspace_aligned and valid_vspace_objs) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned and valid_vspace_objs) s \<Longrightarrow> True \<and> True \<and> (0 < asid \<longrightarrow> ((arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = None \<longrightarrow> True) \<and> (\<forall>x. (arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = Some x \<longrightarrow> (\<forall>pool. ako_at (ASIDPool pool) x s \<longrightarrow> (pool (UCAST(32 \<rightarrow> 10) asid) = None \<longrightarrow> True) \<and> (\<forall>x. pool (UCAST(32 \<rightarrow> 10) asid) = Some x \<longrightarrow> is_aligned x 14)))) \<and> (\<not> 0 < asid \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>pspace_aligned s; valid_vspace_objs s; 0 < asid; asid_table s (asid_high_bits_of asid) = Some x; ako_at (ASIDPool pool) x s; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa\<rbrakk> \<Longrightarrow> is_aligned xa 14 proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>pspace_aligned s; valid_vspace_objs s; 0 < asid; ako_at (ASIDPool pool) x s; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x) s\<rbrakk> \<Longrightarrow> is_aligned xa 14 proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>pspace_aligned s; valid_vspace_objs s; 0 < asid; ako_at (ASIDPool pool) x s; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; valid_vspace_obj (ASIDPool pool) s\<rbrakk> \<Longrightarrow> is_aligned xa 14 proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>pspace_aligned s; valid_vspace_objs s; 0 < asid; ako_at (ASIDPool pool) x s; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; \<forall>x\<in>ran pool. typ_at (AArch APageDirectory) x s\<rbrakk> \<Longrightarrow> is_aligned xa 14 proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>pspace_aligned s; valid_vspace_objs s; 0 < asid; ako_at (ASIDPool pool) x s; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; typ_at (AArch APageDirectory) xa s\<rbrakk> \<Longrightarrow> is_aligned xa 14 proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>pspace_aligned s; valid_vspace_objs s; 0 < asid; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; typ_at (AArch APageDirectory) xa s\<rbrakk> \<Longrightarrow> is_aligned xa 14 proof (prove)
goal (1 subgoal):
 1. \<And>s pool xa pd. \<lbrakk>\<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); valid_vspace_objs s; 0 < asid; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; kheap s xa = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> is_aligned xa 14 proof (prove)
goal (1 subgoal):
 1. \<And>s pool xa pd. \<lbrakk>valid_vspace_objs s; 0 < asid; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; kheap s xa = Some (ArchObj (PageDirectory pd)); is_aligned xa (obj_bits (the (kheap s xa)))\<rbrakk> \<Longrightarrow> is_aligned xa 14 proof (prove)
goal:
No subgoals!