theory VSpace_R

lemma find_pd_for_asid_eq_helper:
  "\<lbrakk> vspace_at_asid asid pd s; valid_vspace_objs s;
         asid \<noteq> 0; pspace_aligned s \<rbrakk>
    \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s
             \<and> page_directory_at pd s \<and> is_aligned pd pdBits" apply (clarsimp simp: vspace_at_asid_def valid_vspace_objs_def) apply (frule spec, drule mp, erule exI) apply (clarsimp simp: vs_asid_refs_def graph_of_def
                 elim!: vs_lookupE) apply (erule rtranclE) apply simp apply (clarsimp dest!: vs_lookup1D) apply (erule rtranclE) defer apply (drule vs_lookup1_trans_is_append') apply (clarsimp dest!: vs_lookup1D) apply (clarsimp dest!: vs_lookup1D) apply (drule spec, drule mp, rule exI,
         rule vs_lookupI[unfolded vs_asid_refs_def]) apply (rule image_eqI[OF refl]) apply (erule graph_ofI) apply clarsimp apply (rule rtrancl.intros(1)) apply (clarsimp simp: vs_refs_def graph_of_def
                 split: Structures_A.kernel_object.splits
                        arch_kernel_obj.splits) apply (clarsimp simp: obj_at_def) apply (drule bspec, erule ranI) apply clarsimp apply (drule ucast_up_inj, simp) apply (simp add: find_pd_for_asid_def bind_assoc
                   word_neq_0_conv[symmetric] liftE_bindE) apply (simp add: exec_gets liftE_bindE bind_assoc
                   get_asid_pool_def get_object_def) apply (simp add: mask_asid_low_bits_ucast_ucast) apply (drule ucast_up_inj, simp) apply (clarsimp simp: returnOk_def get_pde_def
                        get_pd_def get_object_def
                        bind_assoc) apply (frule(1) pspace_alignedD[where p=pd]) apply (simp add: pdBits_def pageBits_def pdeBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vspace_at_asid asid pd s; valid_vspace_objs s; asid \<noteq> 0; pspace_aligned s\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); asid \<noteq> 0; pspace_aligned s\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<in> (vs_lookup1 s)\<^sup>*; asid_table s a = Some b\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ([VSRef (UCAST(7 \<rightarrow> 32) a) None], b) = ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd)\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits
 2. \<And>a b y. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<And>a b y. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pd) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<And>a b p ko. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<in> (vs_lookup1 s)\<^sup>*; ko_at ko p s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits proof (prove)
goal (2 subgoals):
 1. \<And>a b p ko. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko p s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; ([VSRef (UCAST(7 \<rightarrow> 32) a) None], b) = ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p)\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits
 2. \<And>a b p ko y. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko p s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits proof (prove)
goal (2 subgoals):
 1. \<And>a b p ko y. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko p s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; (([VSRef (UCAST(7 \<rightarrow> 32) a) None], b), y) \<in> (vs_lookup1 s)\<^sup>*; (y, [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits
 2. \<And>a b p ko. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko p s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; ([VSRef (UCAST(7 \<rightarrow> 32) a) None], b) = ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p)\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits proof (prove)
goal (2 subgoals):
 1. \<And>a b p ko y. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko p s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; (y, [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<in> vs_lookup1 s; \<exists>zs. fst y = zs @ fst ([VSRef (UCAST(7 \<rightarrow> 32) a) None], b)\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits
 2. \<And>a b p ko. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko p s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; ([VSRef (UCAST(7 \<rightarrow> 32) a) None], b) = ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p)\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<And>a b p ko. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko p s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; ([VSRef (UCAST(7 \<rightarrow> 32) a) None], b) = ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p)\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<And>a b ko. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko b s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits proof (prove)
goal (3 subgoals):
 1. \<And>a b ko. \<lbrakk>asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko b s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> ?ref'76 a b ko \<in> (\<lambda>(r, p). ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` graph_of (asid_table s)
 2. \<And>a b ko. \<lbrakk>asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko b s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> (?ref'76 a b ko, ?rs74 a b ko, ?p69 a b ko) \<in> (vs_lookup1 s)\<^sup>*
 3. \<And>a b ko. \<lbrakk>asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko b s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid); \<forall>ao. ako_at ao (?p69 a b ko) s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits proof (prove)
goal (3 subgoals):
 1. \<And>a b ko. \<lbrakk>asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko b s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> ?x79 a b ko \<in> graph_of (asid_table s)
 2. \<And>a b ko. \<lbrakk>asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko b s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> (case ?x79 a b ko of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p), ?rs74 a b ko, ?p69 a b ko) \<in> (vs_lookup1 s)\<^sup>*
 3. \<And>a b ko. \<lbrakk>asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko b s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid); \<forall>ao. ako_at ao (?p69 a b ko) s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits proof (prove)
goal (2 subgoals):
 1. \<And>a b ko. \<lbrakk>asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko b s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> (case (a, b) of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p), ?rs74 a b ko, ?p69 a b ko) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>a b ko. \<lbrakk>asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko b s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid); \<forall>ao. ako_at ao (?p69 a b ko) s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits proof (prove)
goal (2 subgoals):
 1. \<And>a b ko. \<lbrakk>asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko b s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], b), ?rs74 a b ko, ?p69 a b ko) \<in> (vs_lookup1 s)\<^sup>*
 2. \<And>a b ko. \<lbrakk>asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko b s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid); \<forall>ao. ako_at ao (?p69 a b ko) s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<And>a b ko. \<lbrakk>asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ko_at ko b s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), pd) \<in> vs_refs ko; UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid); \<forall>ao. ako_at ao b s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<And>a b x1 aa. \<lbrakk>UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid); \<forall>ao. ako_at ao b s \<longrightarrow> valid_vspace_obj ao s; asid \<noteq> 0; pspace_aligned s; \<forall>ao. ako_at ao pd s \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; ako_at (arch_kernel_obj.ASIDPool x1) b s; x1 aa = Some pd; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<And>a b x1 aa. \<lbrakk>UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid); \<forall>x\<in>ran x1. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory; asid \<noteq> 0; pspace_aligned s; \<forall>ao. kheap s pd = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; kheap s b = Some (ArchObj (arch_kernel_obj.ASIDPool x1)); x1 aa = Some pd; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> (\<exists>ko. kheap s pd = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<And>a b x1 aa. \<lbrakk>UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid); asid \<noteq> 0; pspace_aligned s; \<forall>ao. kheap s pd = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s; asid_table s a = Some b; kheap s b = Some (ArchObj (arch_kernel_obj.ASIDPool x1)); x1 aa = Some pd; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa; \<exists>ko. kheap s pd = Some ko \<and> a_type ko = AArch APageDirectory\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> (\<exists>ko. kheap s pd = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<And>a b x1 aa pda. \<lbrakk>UCAST(7 \<rightarrow> 32) a = UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid); asid \<noteq> 0; pspace_aligned s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; asid_table s a = Some b; kheap s b = Some (ArchObj (arch_kernel_obj.ASIDPool x1)); x1 aa = Some pd; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa; kheap s pd = Some (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<And>a b x1 aa pda. \<lbrakk>asid \<noteq> 0; pspace_aligned s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; asid_table s a = Some b; kheap s b = Some (ArchObj (arch_kernel_obj.ASIDPool x1)); x1 aa = Some pd; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa; kheap s pd = Some (ArchObj (PageDirectory pda)); a = asid_high_bits_of asid\<rbrakk> \<Longrightarrow> find_pd_for_asid asid s = returnOk pd s \<and> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<And>a b x1 aa pda. \<lbrakk>asid \<noteq> 0; pspace_aligned s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; asid_table s (asid_high_bits_of asid) = Some b; kheap s b = Some (ArchObj (arch_kernel_obj.ASIDPool x1)); x1 aa = Some pd; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa; kheap s pd = Some (ArchObj (PageDirectory pda)); a = asid_high_bits_of asid\<rbrakk> \<Longrightarrow> (do asid_table <- gets (arm_asid_table \<circ> arch_state);
doE pool <- case asid_table (asid_high_bits_of asid) of None \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | Some ptr \<Rightarrow> liftE (get_asid_pool ptr);
case pool (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | Some x2 \<Rightarrow> returnOk x2
odE
od) s = returnOk pd s \<and> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<And>a b x1 aa pda. \<lbrakk>asid \<noteq> 0; pspace_aligned s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; asid_table s (asid_high_bits_of asid) = Some b; kheap s b = Some (ArchObj (arch_kernel_obj.ASIDPool x1)); x1 aa = Some pd; asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) aa; kheap s pd = Some (ArchObj (PageDirectory pda)); a = asid_high_bits_of asid\<rbrakk> \<Longrightarrow> (case x1 (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | Some x2 \<Rightarrow> returnOk x2) s = returnOk pd s \<and> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<And>a b x1 aa pda. \<lbrakk>asid \<noteq> 0; pspace_aligned s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; asid_table s (asid_high_bits_of asid) = Some b; kheap s b = Some (ArchObj (arch_kernel_obj.ASIDPool x1)); x1 aa = Some pd; UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) asid) = UCAST(10 \<rightarrow> 32) aa; kheap s pd = Some (ArchObj (PageDirectory pda)); a = asid_high_bits_of asid\<rbrakk> \<Longrightarrow> (case x1 (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | Some x2 \<Rightarrow> returnOk x2) s = returnOk pd s \<and> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<And>a b x1 aa pda. \<lbrakk>asid \<noteq> 0; pspace_aligned s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; asid_table s (asid_high_bits_of asid) = Some b; kheap s b = Some (ArchObj (arch_kernel_obj.ASIDPool x1)); x1 aa = Some pd; kheap s pd = Some (ArchObj (PageDirectory pda)); a = asid_high_bits_of asid; UCAST(32 \<rightarrow> 10) asid = aa\<rbrakk> \<Longrightarrow> (case x1 (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | Some x2 \<Rightarrow> returnOk x2) s = returnOk pd s \<and> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<And>b x1 pda. \<lbrakk>asid \<noteq> 0; pspace_aligned s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; asid_table s (asid_high_bits_of asid) = Some b; kheap s b = Some (ArchObj (arch_kernel_obj.ASIDPool x1)); x1 (UCAST(32 \<rightarrow> 10) asid) = Some pd; kheap s pd = Some (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> is_aligned pd pdBits proof (prove)
goal (1 subgoal):
 1. \<And>b x1 pda. \<lbrakk>asid \<noteq> 0; pspace_aligned s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; asid_table s (asid_high_bits_of asid) = Some b; kheap s b = Some (ArchObj (arch_kernel_obj.ASIDPool x1)); x1 (UCAST(32 \<rightarrow> 10) asid) = Some pd; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd (obj_bits (ArchObj (PageDirectory pda)))\<rbrakk> \<Longrightarrow> is_aligned pd pdBits proof (prove)
goal:
No subgoals!